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

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

tests
0

failures
0

ignored
14m29.96s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.250s passed
powPositiveConcrete data()[101] 4.290s passed
powGeq1Concrete data()[102] 4.150s passed
pow2InIntLower data()[103] 4.173s passed
pow2InIntUpper data()[104] 4.191s passed
logSelfConcrete data()[105] 4.200s passed
log1Concrete data()[106] 4.255s passed
logProduct data()[107] 4.171s passed
logTimesBaseConcrete data()[108] 4.194s passed
logProdIdentity data()[109] 4.227s passed
moduloByteIsInByte data()[10] 4.343s passed
logProdIdentityConcrete data()[110] 4.191s passed
logPowIdentity data()[111] 4.207s passed
logPowIdentityConcrete data()[112] 4.161s passed
logPositive data()[113] 4.290s passed
logPositiveConcrete data()[114] 4.228s passed
logMono data()[115] 4.240s passed
logMonoConcrete data()[116] 4.223s passed
powLogLess data()[117] 4.174s passed
powLogMore2 data()[118] 4.198s passed
logLessThanPow data()[119] 4.298s passed
moduloCharIsInChar data()[11] 4.397s passed
logLessThanPowConcrete data()[120] 4.222s passed
logSqueeze data()[121] 4.146s passed
ifthenelse_equals data()[122] 4.124s passed
ifthenelse_equals_1 data()[123] 4.202s passed
ifthenelse_equals_2 data()[124] 4.113s passed
disjointWithSingleton1 data()[125] 4.139s passed
disjointWithSingleton2 data()[126] 4.124s passed
disjointArrayRanges data()[127] 4.160s passed
disjointArrayRangeAllFields1 data()[128] 4.236s passed
disjointArrayRangeAllFields2 data()[129] 4.214s passed
div_unique1 data()[12] 4.400s passed
seqSelfDefinition data()[130] 4.245s passed
seqOutsideValue data()[131] 4.236s passed
castedGetAny data()[132] 4.320s passed
seqGetAlphaCast data()[133] 4.264s passed
getOfSeqSingleton data()[134] 4.139s passed
getOfSeqSingletonConcrete data()[135] 4.175s passed
getOfSeqConcat data()[136] 4.248s passed
getOfSeqSub data()[137] 4.262s passed
getOfSeqReverse data()[138] 4.236s passed
lenOfSeqEmpty data()[139] 4.222s passed
div_unique2 data()[13] 4.284s passed
lenOfSeqSingleton data()[140] 4.197s passed
lenOfSeqConcat data()[141] 4.136s passed
lenOfSeqSub data()[142] 4.344s passed
lenOfSeqReverse data()[143] 4.176s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.258s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.201s passed
getOfSeqSingletonEQ data()[146] 4.148s passed
getOfSeqConcatEQ data()[147] 4.264s passed
getOfSeqSubEQ data()[148] 4.185s passed
getOfSeqReverseEQ data()[149] 4.158s passed
div_exists data()[14] 4.528s passed
lenOfSeqEmptyEQ data()[150] 4.212s passed
lenOfSeqSingletonEQ data()[151] 4.195s passed
lenOfSeqConcatEQ data()[152] 4.238s passed
lenOfSeqSubEQ data()[153] 4.197s passed
lenOfSeqReverseEQ data()[154] 4.164s passed
getOfSeqDefEQ data()[155] 4.216s passed
lenOfSeqDefEQ data()[156] 4.322s passed
seqConcatWithSeqEmpty1 data()[157] 4.257s passed
seqConcatWithSeqEmpty2 data()[158] 4.263s passed
seqReverseOfSeqEmpty data()[159] 4.278s passed
div_one data()[15] 4.429s passed
subSeqComplete data()[160] 4.308s passed
subSeqTailR data()[161] 4.256s passed
subSeqTailL data()[162] 4.320s passed
subSeqTailEQR data()[163] 4.258s passed
subSeqTailEQL data()[164] 4.134s passed
seqDef_split data()[165] 4.236s passed
seqDef_induction_upper data()[166] 4.244s passed
seqDef_induction_upper_concrete data()[167] 4.223s passed
seqDef_induction_lower data()[168] 4.272s passed
seqDef_induction_lower_concrete data()[169] 4.206s passed
jdiv_one data()[16] 4.311s passed
seqDef_split_in_three data()[170] 4.327s passed
seqDef_empty data()[171] 4.194s passed
seqDef_one_summand data()[172] 4.213s passed
seqDef_lower_equals_upper data()[173] 4.294s passed
seqDefOfSeq data()[174] 4.237s passed
seqSelfDefinitionEQ2 data()[175] 4.284s passed
indexOfSeqSingleton data()[176] 4.211s passed
indexOfSeqConcatFirst data()[177] 4.215s passed
indexOfSeqConcatSecond data()[178] 4.163s passed
indexOfSeqSub data()[179] 4.194s passed
div_zero data()[17] 4.399s passed
lenOfArray2seq data()[180] 4.313s passed
getAnyOfArray2seq data()[181] 4.218s passed
getOfArray2seq data()[182] 4.162s passed
getAnyOfNPermInv data()[183] 4.195s passed
seqNPermRange data()[184] 4.303s passed
seqPermTrans data()[185] 4.299s passed
seqPermRefl data()[186] 4.330s passed
seqPermSplit data()[187] 4.315s passed
seqNPermRight data()[188] 4.372s passed
seqPermFromSwap data()[189] 4.333s passed
divResZero1 data()[18] 4.354s passed
seqPermTransAlt0 data()[190] 4.319s passed
seqPermTransAlt1 data()[191] 4.252s passed
seqPermTransAlt2 data()[192] 4.202s passed
seqPermTransAlt3 data()[193] 4.165s passed
seqPermForall data()[194] 4.357s passed
seqPermExists data()[195] 4.290s passed
schiffl_lemma_2 data()[196] 28.799s passed
schiffl_thm_1 data()[197] 5.214s passed
eqSameSeq data()[198] 4.419s passed
divResZero2 data()[19] 4.283s passed
eqTermCut data()[1] 5.551s passed
divResOne1 data()[20] 4.326s passed
divResOne2 data()[21] 4.311s passed
div_cancel1 data()[22] 4.274s passed
div_cancel2 data()[23] 4.271s passed
divAddMultDenom data()[24] 4.289s passed
divMinus data()[25] 4.263s passed
divMinusDenom data()[26] 4.357s passed
divLeastDPos data()[27] 4.251s passed
divLeastDNeg data()[28] 4.264s passed
divGreatestDPos data()[29] 4.358s passed
equivAllRight data()[2] 4.740s passed
divGreatestDNeg data()[30] 4.285s passed
divIncreasingPos data()[31] 4.385s passed
divIncreasingNeg data()[32] 4.385s passed
jdiv_zero data()[33] 4.391s passed
jdivPulloutMinusNum data()[34] 4.218s passed
jdivPulloutMinusDenom data()[35] 4.416s passed
jdiv_uniquePosPos data()[36] 4.207s passed
jdiv_uniquePosNeg data()[37] 4.215s passed
jdiv_uniqueNegPos data()[38] 4.290s passed
jdiv_uniqueNegNeg data()[39] 4.186s passed
irrflConcrete1 data()[3] 4.664s passed
jdivMultDenom1 data()[40] 4.226s passed
jdivMultDenom2 data()[41] 4.344s passed
mod_geZero data()[42] 4.320s passed
mod_lessDenom data()[43] 4.299s passed
jmod_NumPos data()[44] 4.260s passed
jmod_NumNeg data()[45] 4.249s passed
jmod_geZero data()[46] 4.237s passed
jmodNumZero data()[47] 4.272s passed
jmod_pulloutminusNum data()[48] 4.227s passed
jmod_pulloutminusDenom data()[49] 4.127s passed
irrflConcrete2 data()[4] 4.548s passed
jmodUnique1 data()[50] 4.188s passed
jmodUnique2 data()[51] 4.219s passed
intDivRem data()[52] 4.245s passed
jmodjmod data()[53] 4.206s passed
jmodDivisible data()[54] 4.264s passed
jmodDivisibleRep data()[55] 4.203s passed
jdivAddMultDenom data()[56] 4.318s passed
jmodAltZero data()[57] 4.251s passed
jmodAddMultDenomZero data()[58] 4.215s passed
polyDiv_zero data()[59] 4.264s passed
cancel_gtPos data()[5] 4.585s passed
polyMod_ltdivDenom data()[60] 4.208s passed
bsum_empty data()[61] 4.225s passed
bsum_induction_upper data()[62] 4.310s passed
bsum_induction_lower data()[63] 4.222s passed
bsum_num_of_bounds data()[64] 4.213s passed
bsum_num_of_bounds2 data()[65] 4.291s passed
bsum_induction_upper2 data()[66] 4.204s passed
bsum_induction_upper_concrete data()[67] 4.187s passed
bsum_induction_upper_concrete_2 data()[68] 4.132s passed
bsum_induction_upper2_concrete data()[69] 4.200s passed
cancel_gtNeg data()[6] 4.536s passed
bsum_induction_lower_concrete data()[70] 4.175s passed
bsum_induction_lower2 data()[71] 4.262s passed
bsum_induction_lower2_concrete data()[72] 4.217s passed
bsum_positive data()[73] 4.245s passed
bsum_upper_bound data()[74] 4.298s passed
bsum_lower_bound data()[75] 4.221s passed
bsum_positive_lower_bound_element data()[76] 4.248s passed
bsum_sub_same_index data()[77] 4.288s passed
bsum_less_same_index data()[78] 4.282s passed
bsum_equal_except_one_index data()[79] 4.225s passed
moduloIntIsInInt data()[7] 4.325s passed
bsum_num_of_is_max data()[80] 4.201s passed
bsum_num_of_is_max2 data()[81] 4.184s passed
bsum_num_of_is_max3 data()[82] 4.220s passed
bsum_num_of_is_max4 data()[83] 4.292s passed
bsum_num_of_lt_max data()[84] 4.213s passed
bsum_num_of_lt_max2 data()[85] 4.302s passed
bsum_num_of_lt_max3 data()[86] 4.353s passed
bsum_num_of_lt_max4 data()[87] 4.259s passed
bsum_num_of_gt0 data()[88] 4.232s passed
bsum_num_of_gt0_alt data()[89] 4.293s passed
moduloLongIsInLong data()[8] 4.350s passed
bsum_add_concrete data()[90] 4.244s passed
bprod_all_positive data()[91] 4.245s passed
bprod_split data()[92] 4.236s passed
powConcrete0 data()[93] 4.192s passed
powConcrete1 data()[94] 4.189s passed
powSplitFactor data()[95] 4.180s passed
powAdd data()[96] 4.201s passed
powMono data()[97] 4.176s passed
powMonoConcrete data()[98] 4.181s passed
powMonoConcreteRight data()[99] 4.270s passed
moduloShortIsInShort data()[9] 4.343s passed

Standard output

497        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
533        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 12.94ms 
808        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
826        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)

2075       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2077       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2089       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2090       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4148       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11183      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.37s 
11280      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11329      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.9ns 
11343      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11343      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.3ns 
11349      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15447      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.1s 
15452      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16885      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.67ms 
16905      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16905      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.1ns 
16907      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20431      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
20432      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21626      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21643      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.91ms 
21648      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21649      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 403.4ns 
21651      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25201      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.55s 
25201      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
26300      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
26308      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 
26312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
26312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 431.8ns 
26314      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29744      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.43s 
29744      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30851      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
30858      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
30863      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
30864      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 617.4ns 
30866      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34317      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
34318      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
35395      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
35443      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.3ms 
35449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
35449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 446.2ns 
35451      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38780      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
38781      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
39918      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
39982      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.66ms 
39985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
39985      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.2ns 
39987      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43240      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
43241      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
44304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
44308      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 942.9ns 
44310      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
44311      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.1ns 
44312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47596      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
47596      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
48653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
48658      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 865.5ns 
48660      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
48661      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.4ns 
48662      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51950      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
51951      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
52996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
53000      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712.2ns 
53003      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
53004      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.4ns 
53005      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56309      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
56310      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
57340      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
57344      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 799.3ns 
57347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
57347      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.1ns 
57348      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60624      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
60625      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
61738      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
61741      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 876.49ns 
61745      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
61745      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.3ns 
61746      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64978      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
64979      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
66060      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
66140      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.53ms 
66146      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
66147      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.4ns 
66148      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69355      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
69356      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
70391      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
70428      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.69ms 
70430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
70431      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.3ns 
70432      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73629      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
73629      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
74687      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
74955      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 256.17ms 
74959      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
74960      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.8ns 
74961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78339      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
78339      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
79380      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
79387      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
79389      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
79389      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.6ns 
79391      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82671      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
82672      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
83694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
83698      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
83702      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
83703      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.4ns 
83704      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86954      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
86955      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
88020      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
88097      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.2ms 
88103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
88103      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 433ns 
88105      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91361      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
91362      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
92435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
92454      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.66ms 
92457      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
92457      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.2ns 
92458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95666      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
95667      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
96719      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
96737      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.93ms 
96741      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
96741      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.1ns 
96742      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
100003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
101043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
101064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.28ms 
101066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
101067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 423.6ns 
101068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
104361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
105354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
105375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms 
105378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
105384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.01ms 
105385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
108587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
109621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
109648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.97ms 
109652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
109657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.65ms 
109658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
112879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
113908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
113920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
113923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
113923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.1ns 
113925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
117131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
118159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
118208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.88ms 
118211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
118211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.9ns 
118213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
121360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
122395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
122471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.46ms 
122474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
122475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.3ns 
122476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
125717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
126780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
126828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.02ms 
126831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
126831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.89ns 
126833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
130056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
131067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
131080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.24ms 
131082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
131082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.1ns 
131083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
134296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
135327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
135344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.71ms 
135346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
135346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
135347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
138634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
139689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
139702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.5ms 
139703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
139704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
139704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
142913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
143978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
143987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.54ms 
143989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
143989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
143990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
147259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
148354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
148370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.99ms 
148375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
148376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.4ns 
148377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
151690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
152750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
152758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
152760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
152760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.1ns 
152761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
156119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
157145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
157149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
157150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
157151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.3ns 
157151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
160355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
161355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
161368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.17ms 
161369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
161370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.5ns 
161371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
164647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
165726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
165779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.89ms 
165785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
165786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.2ns 
165788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
168941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
169965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
169990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.6ms 
169992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
169993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.6ns 
169994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
173147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
174184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
174205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.97ms 
174207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
174208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.39ns 
174209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
177429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
178474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
178495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.05ms 
178497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
178497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.3ns 
178498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
181670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
182661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
182681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.73ms 
182682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
182682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
182683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
185844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
186844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
186905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.92ms 
186912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
186912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.5ns 
186914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
190174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
191249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
191252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
191255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
191255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306ns 
191257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
194462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
195567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
195573     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
195575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
195575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.1ns 
195576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
198815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
199862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
199872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.02ms 
199875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
199875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 323.8ns 
199877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
203119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
204125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
204133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.14ms 
204135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
204135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.2ns 
204136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
207360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
208360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
208382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.07ms 
208383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
208383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
208384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
211625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
212609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
212618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.46ms 
212621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
212621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.5ns 
212622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
215789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
216885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
216891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
216893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
216894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.9ns 
216895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
220079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
221114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
221118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
221120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
221120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
221121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
224237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
225241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
225246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
225247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
225247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
225248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
228354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
229348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
229433     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.8ms 
229434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
229435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.3ns 
229436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
232572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
233551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
233652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 90.66ms 
233654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
233654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.5ns 
233655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
236849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
237893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
237897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
237899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
237899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.1ns 
237900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
241067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
242063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
242102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.86ms 
242105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
242106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 474.5ns 
242107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
245305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
246336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
246367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.84ms 
246369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
246369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns 
246370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
249544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
250566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
250570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
250572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
250572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
250573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
253724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
254737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
254887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 134.15ms 
254890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
254891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.4ns 
254892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
258110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
259127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
259139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.12ms 
259141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
259141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
259142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
262338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
263346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
263355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
263356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
263356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.3ns 
263357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
266578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
267599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
267619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.46ms 
267620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
267620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
267621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
270805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
271811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
271826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.69ms 
271828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
271828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
271829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
275015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
276046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
276051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
276052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
276053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
276053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
279302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
280356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
280362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
280363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
280363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
280364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
283568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
284563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
284583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.4ms 
284585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
284585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
284586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
287785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
288779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
288796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.56ms 
288800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
288800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.9ns 
288801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
292055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
293073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
293089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.67ms 
293091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
293091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
293092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
296276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
297288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
297293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
297295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
297296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.6ns 
297297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
300431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
301477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
301480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
301482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
301482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
301483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
304588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
305606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
305613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.97ms 
305614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
305614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
305615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
308814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
309809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
309812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
309815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
309815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.1ns 
309816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
312975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
313985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
313987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 570.6ns 
313989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
313989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
313990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
317244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
318245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
318249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
318251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
318251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
318252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
321435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
322464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
322467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 845.2ns 
322468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
322468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
322469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
325593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
326629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
326711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.07ms 
326714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
326714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.3ns 
326715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
329923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
330961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
331010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.02ms 
331011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
331011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
331012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
334196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
335191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
335230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.6ms 
335232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
335232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.7ns 
335234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
338435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
339430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
339478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.09ms 
339480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
339481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
339481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
342692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
343737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
343766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.32ms 
343767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
343767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
343768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
346947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
347990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
348048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.52ms 
348050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
348050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
348051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
351218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
352242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
352273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.17ms 
352275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
352275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.8ns 
352276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
355438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
356454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
356474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ms 
356476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
356476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
356477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
359631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
360635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
360658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.86ms 
360660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
360660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns 
360661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
363846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
364860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
364879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.42ms 
364880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
364880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.41ns 
364881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
368093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
369145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
369170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.94ms 
369172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
369172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
369173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
372332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
373359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
373383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.96ms 
373385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
373385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
373386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
376613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
377650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
377683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.91ms 
377687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
377687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.4ns 
377690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
380944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
382014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
382038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.07ms 
382040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
382040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
382041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
385275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
386278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
386297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.87ms 
386299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
386299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
386300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
389472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
390507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
390529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.13ms 
390531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
390531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.4ns 
390532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
393726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
394801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
394822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.38ms 
394824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
394824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
394825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
398023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
399059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
399066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
399068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
399068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
399069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
402258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
403294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
403311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.61ms 
403312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
403313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
403313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
406487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
407543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
407547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
407549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
407549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
407550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
410753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
411736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
411739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 992.8ns 
411740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
411741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
411741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
414898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
415923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
415928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 875.2ns 
415930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
415930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
415931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
419097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
420099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
420108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.52ms 
420110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
420110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
420111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
423262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
424301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
424309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
424311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
424311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.9ns 
424312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
427439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
428471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
428485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.61ms 
428486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
428486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
428487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
431652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
432663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
432667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
432668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
432668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
432669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
435910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
436934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
436936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 542.2ns 
436938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
436938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
436939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
440151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
441180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
441186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ms 
441187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
441187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
441189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
444456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
445473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
445476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 948.9ns 
445477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
445477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
445478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
448615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
449624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
449626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.2ns 
449628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
449628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
449628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
452787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
453797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
453800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 706ns 
453801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
453801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
453802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
456945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
457986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
457991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
457992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
457992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
457993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
461189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
462181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
462191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.41ms 
462192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
462192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
462193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
465435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
466441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
466445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
466446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
466446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
466447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
469588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
470607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
470616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.57ms 
470617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
470617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
470618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
473774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
474804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
474810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
474812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
474812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.1ns 
474813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
477980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
479020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
479037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.01ms 
479039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
479039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
479040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
482228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
483224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
483229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
483230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
483230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
483231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
486401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
487432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
487435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
487437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
487437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
487438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
490611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
491592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
491596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
491597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
491597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
491598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
494780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
495866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
495885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.56ms 
495889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
495889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.7ns 
495890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
499076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
500108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
500113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 524.8ns 
500116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
500116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
500117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
503308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
504318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
504354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.51ms 
504356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
504356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
504357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
507508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
508573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
508578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
508579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
508579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
508580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
511740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
512730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
512751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.6ms 
512753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
512753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
512753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
515952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
516930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
516949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.32ms 
516950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
516950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
516951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
520163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
521224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
521248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.88ms 
521249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
521249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
521250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
524435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
525464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
525468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 563.9ns 
525471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
525472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.4ns 
525473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
528593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
529609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
529615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.93ms 
529617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
529617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
529618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
532757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
533735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
533739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
533740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
533741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
533741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
536926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
537938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
537941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 944ns 
537943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
537943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
537944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
541035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
542052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
542055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
542056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
542056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
542057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
545175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
546188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
546193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
546195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
546195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
546196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
549323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
550315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
550318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
550319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
550319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
550320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
553445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
554467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
554477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.9ms 
554478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
554478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
554479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
557670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
558705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
558714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.07ms 
558715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
558715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
558716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
561863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
562917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
562927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.96ms 
562929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
562929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
562930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
566132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
567163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
567172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.35ms 
567173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
567173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
567174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
570334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
571403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
571408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
571410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
571410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.8ns 
571411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
574614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
575724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
575729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
575730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
575730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
575731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
578935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
579990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
579993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 939ns 
579994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
579994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
579995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
583095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
584128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
584131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
584133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
584133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
584134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
587270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
588304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
588306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
588308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
588308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
588308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
591493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
592542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
592554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.44ms 
592556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
592556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
592557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
595768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
596813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
596817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
596818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
596818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
596819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
600020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
601045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
601052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.47ms 
601054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
601054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns 
601055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
604224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
605272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
605275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 913.3ns 
605276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
605276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
605277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
608435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
609468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
609471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 838ns 
609472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
609473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.6ns 
609473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
612587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
613603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
613606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
613609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
613609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
613610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
616914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
617949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
617952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 999.71ns 
617953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
617953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.9ns 
617954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
621083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
622124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
622128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
622129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
622129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
622130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
625310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
626382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
626385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
626387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
626387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
626388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
629574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
630582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
630586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
630588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
630588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
630589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
633695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
634731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
634734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
634736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
634736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
634737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
637954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
638985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
638999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.43ms 
639000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
639000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
639001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
642165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
643181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
643183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 600.1ns 
643184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
643184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
643185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
646310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
647334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
647341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.16ms 
647343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
647343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
647344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
650527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
651551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
651553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
651555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
651555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
651555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
654722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
655746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
655749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 948.9ns 
655750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
655750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
655751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
658947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
659982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
659987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
659988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
659988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
659989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
663124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
664180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
664183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
664185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
664185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
664185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
667308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
668344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
668347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
668348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
668348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
668349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
671496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
672558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
672563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
672568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
672568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 263.3ns 
672569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
675805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
676883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
676888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
676889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
676890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.7ns 
676890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
680096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
681135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
681145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.43ms 
681147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
681147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
681148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
684349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
685390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
685408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.37ms 
685410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
685410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
685411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
688616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
689679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
689687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.76ms 
689688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
689688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
689689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
692937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
693981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
693994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.71ms 
693996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
693997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.6ns 
693998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
697176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
698237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
698250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.78ms 
698252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
698252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
698253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
701527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
702557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
702571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.92ms 
702572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
702572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
702573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
705736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
706815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
706828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.24ms 
706830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
706830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
706830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
709941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
710953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
710963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.12ms 
710964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
710964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
710965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
714095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
714095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
715170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
715198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.03ms 
715199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
715199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
715200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
718384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
718384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
719414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
719442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.96ms 
719444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
719444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
719445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
722625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
723639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
723665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.28ms 
723667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
723667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
723668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
726842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
727910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
727937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.19ms 
727939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
727939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
727941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
731098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
732116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
732143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.33ms 
732144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
732145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
732146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
735312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
736403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
736469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.1ms 
736471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
736471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
736472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
739611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
740658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
740664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.67ms 
740666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
740666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
740667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
743811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
744871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
744877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.12ms 
744879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
744879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
744879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
748118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
749167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
749171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
749173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
749173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
749174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
752358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
753391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
753408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.51ms 
753410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
753410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 
753411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
756617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
757677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
757686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.46ms 
757694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
757694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.6ns 
757695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
760860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
760860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
761900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
761904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
761905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
761905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.6ns 
761906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
765052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
766105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
766118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.12ms 
766119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
766119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
766120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
769235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
769235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
770268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
770281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.84ms 
770283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
770283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
770284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
773428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
774457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
774475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.28ms 
774476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
774477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
774477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
777713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
777713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
778784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
778788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
778789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
778789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
778790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
781962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
781962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
783002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
783007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
783008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
783008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
783009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
786119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
786119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
787162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
787168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
787170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
787170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
787171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
790306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
790306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
791357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
791363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms 
791365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
791365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
791366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
794522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
794523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
795602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
795666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.03ms 
795667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
795668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
795668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
798889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
798889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
799938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
799965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.49ms 
799967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
799967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
799967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
803199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
803199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
804279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
804296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.7ms 
804297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
804297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.5ns 
804298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
807554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
807554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
808608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
808611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 268ns 
808612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
808612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
808613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
811825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
811825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
812869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
812982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 98.8ms 
812984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
812984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.6ns 
812985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
816220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
816221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
817266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
817315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.57ms 
817317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
817317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
817318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
820533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
820533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
821632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
821634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 253.4ns 
821636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
821636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
821636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
824824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
824825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
825884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
825886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 303.4ns 
825888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
825888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
825888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
829057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
829057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
830086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
830088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 263.8ns 
830090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
830090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
830091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
833217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
833218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
834251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
834253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 426.8ns 
834254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
834255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
834255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
837428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
837429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
838474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
838599     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
838609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 131.89ms 
838613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
838613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.4ns 
838617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
841816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
841817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
842846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
842900     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
842901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.18ms 
842904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
842904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.9ns 
842905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
846095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
846095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
847131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
847133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ns 
847169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
847238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
847257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
847265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
847281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
847282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
847284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
847286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
847292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
847293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
847298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
847300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
847602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
847604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
847606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
847607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
847609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
847787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
847788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
847792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
847793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
847795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
847797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
848020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
848022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
848024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
848024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
848026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
848031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
848198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
848199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
848205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
848206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
848207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
848208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
848221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
848222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
848223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
848225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
848228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
848229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
848240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
848242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
848243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
848244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
848244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
848245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
848422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
848423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
848425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
848592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
848594     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)'' 
848596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
848599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
848599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
848601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
848602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
848605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
848610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
848611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
848612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
848614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
848615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
848769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
848774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
848776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
848777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
848778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
848779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
848781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
848960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
848961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
848962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
848964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
848965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
848965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
848967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
848969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
849126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
849130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
849341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
849346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
849356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
849357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
849361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
849363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
849364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
849364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
849365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
849366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
849379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
849385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
849520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
849521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
849524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
849526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
849527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
849528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
849528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
849529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
849647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
849657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
849816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
849817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
849819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
849821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
849822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
849823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
849992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
849997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
850001     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)'' 
850003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
850005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
850006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
850006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
850007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
850021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
850028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
850029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
850030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
850152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
850154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
850155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
850157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
850157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
850159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
850288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
850289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
850291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
850293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
850293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
850294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
850295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
850296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
850404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
850406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
850503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
850504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
850505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
850510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
850515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
850521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
850680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
850681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
850682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
850683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
850696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
850807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
855574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
855575     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)'' 
855580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
855582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
855583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
855583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
855585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
855598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
855599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
855600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
855601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
855602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
855727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
855732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
855733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
855735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
855735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
855736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
855737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
855867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
855868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
855869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
855872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
855873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
855874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
855876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
855877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
856001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
856002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
856111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
856117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
856124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
856125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
856125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
856127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
856140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
856254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
856255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
856256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
856257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
856359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
856372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
856373     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)'' 
856374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
856375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
856376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
856376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
856377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
856391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
856392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
856393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
856394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
856394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
856513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
856514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
856515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
856516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
856517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
856643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
856650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
856651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
856652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
856653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
856654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
856655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
856807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
856808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
856809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
856810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
856810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
856811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
856812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
856812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
856813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
856814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
856815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
856815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
856816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
856816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
856817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
856935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
856936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
856944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
857050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
857156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
857157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
857158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
857159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
857160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
857160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
857161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
857161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
857162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
857274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
857282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
857403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
857404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
857404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
857405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
857406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
857407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
857407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
857408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
857414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
857415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
857571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
857577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
857585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
857710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
857711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
857712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
857713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
857713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
857714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
857714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
857715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
857785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
857786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
857787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
857787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
857788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
857795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
857802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
857952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
858064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
858065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
858066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
858067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
858277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
858389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
858390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
862233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
862238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
862239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
862240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
862241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
862384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
862385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
862387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
862387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
862388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
862521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
866100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
870103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
870107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
870108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
870109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
870110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
870250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
870250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
870251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
870252     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)' ...' 
870253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
871704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
871704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132ns 
871707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
874982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
874983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
876111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
876112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 
876113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
876123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
876133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
876135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
876137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
876139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
876144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
876145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
876150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
876151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
876153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
876165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
876165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
876167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
876223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
876224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
876224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
876225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
876226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
876308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
876308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
876309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
876312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
876313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
876318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
876319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
876319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
876319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
876320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
876321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
876419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
876420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
876420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
876421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
876423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
876424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
876527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
876527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
876528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
876528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
876529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
876529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
876530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
876530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
876531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
876531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
876532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
876532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
876533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
876533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
876534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
876534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
876534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
876535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
876536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
876539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
876575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
876576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
876632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
876633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
876634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
876635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
876636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
876637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
876692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
876695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
876696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
876697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
876698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
876699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
876700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
876754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
876758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
876762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
876839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
876916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
876916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.3ns 
876917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
880175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
880175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
881311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
881333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.3ms