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

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

tests
0

failures
0

ignored
14m31.57s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.182s passed
powPositiveConcrete data()[101] 4.134s passed
powGeq1Concrete data()[102] 4.165s passed
pow2InIntLower data()[103] 4.190s passed
pow2InIntUpper data()[104] 4.126s passed
logSelfConcrete data()[105] 4.123s passed
log1Concrete data()[106] 4.215s passed
logProduct data()[107] 4.232s passed
logTimesBaseConcrete data()[108] 4.288s passed
logProdIdentity data()[109] 4.223s passed
moduloByteIsInByte data()[10] 4.350s passed
logProdIdentityConcrete data()[110] 4.199s passed
logPowIdentity data()[111] 4.182s passed
logPowIdentityConcrete data()[112] 4.203s passed
logPositive data()[113] 4.176s passed
logPositiveConcrete data()[114] 4.151s passed
logMono data()[115] 4.271s passed
logMonoConcrete data()[116] 4.365s passed
powLogLess data()[117] 4.291s passed
powLogMore2 data()[118] 4.271s passed
logLessThanPow data()[119] 4.298s passed
moduloCharIsInChar data()[11] 4.345s passed
logLessThanPowConcrete data()[120] 4.328s passed
logSqueeze data()[121] 4.169s passed
ifthenelse_equals data()[122] 4.211s passed
ifthenelse_equals_1 data()[123] 4.183s passed
ifthenelse_equals_2 data()[124] 4.180s passed
disjointWithSingleton1 data()[125] 4.184s passed
disjointWithSingleton2 data()[126] 4.182s passed
disjointArrayRanges data()[127] 4.183s passed
disjointArrayRangeAllFields1 data()[128] 4.138s passed
disjointArrayRangeAllFields2 data()[129] 4.227s passed
div_unique1 data()[12] 4.371s passed
seqSelfDefinition data()[130] 4.306s passed
seqOutsideValue data()[131] 4.285s passed
castedGetAny data()[132] 4.313s passed
seqGetAlphaCast data()[133] 4.249s passed
getOfSeqSingleton data()[134] 4.308s passed
getOfSeqSingletonConcrete data()[135] 4.269s passed
getOfSeqConcat data()[136] 4.235s passed
getOfSeqSub data()[137] 4.281s passed
getOfSeqReverse data()[138] 4.111s passed
lenOfSeqEmpty data()[139] 4.147s passed
div_unique2 data()[13] 4.435s passed
lenOfSeqSingleton data()[140] 4.148s passed
lenOfSeqConcat data()[141] 4.128s passed
lenOfSeqSub data()[142] 4.138s passed
lenOfSeqReverse data()[143] 4.170s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.256s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.219s passed
getOfSeqSingletonEQ data()[146] 4.208s passed
getOfSeqConcatEQ data()[147] 4.250s passed
getOfSeqSubEQ data()[148] 4.200s passed
getOfSeqReverseEQ data()[149] 4.226s passed
div_exists data()[14] 4.525s passed
lenOfSeqEmptyEQ data()[150] 4.190s passed
lenOfSeqSingletonEQ data()[151] 4.283s passed
lenOfSeqConcatEQ data()[152] 4.234s passed
lenOfSeqSubEQ data()[153] 4.165s passed
lenOfSeqReverseEQ data()[154] 4.145s passed
getOfSeqDefEQ data()[155] 4.170s passed
lenOfSeqDefEQ data()[156] 4.220s passed
seqConcatWithSeqEmpty1 data()[157] 4.165s passed
seqConcatWithSeqEmpty2 data()[158] 4.186s passed
seqReverseOfSeqEmpty data()[159] 4.339s passed
div_one data()[15] 4.384s passed
subSeqComplete data()[160] 4.329s passed
subSeqTailR data()[161] 4.318s passed
subSeqTailL data()[162] 4.298s passed
subSeqTailEQR data()[163] 4.260s passed
subSeqTailEQL data()[164] 4.155s passed
seqDef_split data()[165] 4.279s passed
seqDef_induction_upper data()[166] 4.235s passed
seqDef_induction_upper_concrete data()[167] 4.339s passed
seqDef_induction_lower data()[168] 4.432s passed
seqDef_induction_lower_concrete data()[169] 4.380s passed
jdiv_one data()[16] 4.272s passed
seqDef_split_in_three data()[170] 4.395s passed
seqDef_empty data()[171] 4.203s passed
seqDef_one_summand data()[172] 4.174s passed
seqDef_lower_equals_upper data()[173] 4.197s passed
seqDefOfSeq data()[174] 4.235s passed
seqSelfDefinitionEQ2 data()[175] 4.217s passed
indexOfSeqSingleton data()[176] 4.228s passed
indexOfSeqConcatFirst data()[177] 4.335s passed
indexOfSeqConcatSecond data()[178] 4.190s passed
indexOfSeqSub data()[179] 4.309s passed
div_zero data()[17] 4.239s passed
lenOfArray2seq data()[180] 4.250s passed
getAnyOfArray2seq data()[181] 4.202s passed
getOfArray2seq data()[182] 4.300s passed
getAnyOfNPermInv data()[183] 4.210s passed
seqNPermRange data()[184] 4.350s passed
seqPermTrans data()[185] 4.271s passed
seqPermRefl data()[186] 4.224s passed
seqPermSplit data()[187] 4.224s passed
seqNPermRight data()[188] 4.563s passed
seqPermFromSwap data()[189] 4.299s passed
divResZero1 data()[18] 4.290s passed
seqPermTransAlt0 data()[190] 4.216s passed
seqPermTransAlt1 data()[191] 4.245s passed
seqPermTransAlt2 data()[192] 4.282s passed
seqPermTransAlt3 data()[193] 4.280s passed
seqPermForall data()[194] 4.387s passed
seqPermExists data()[195] 4.368s passed
schiffl_lemma_2 data()[196] 29.406s passed
schiffl_thm_1 data()[197] 5.288s passed
eqSameSeq data()[198] 4.458s passed
divResZero2 data()[19] 4.275s passed
eqTermCut data()[1] 5.080s passed
divResOne1 data()[20] 4.409s passed
divResOne2 data()[21] 4.583s passed
div_cancel1 data()[22] 4.296s passed
div_cancel2 data()[23] 4.313s passed
divAddMultDenom data()[24] 4.407s passed
divMinus data()[25] 4.355s passed
divMinusDenom data()[26] 4.410s passed
divLeastDPos data()[27] 4.283s passed
divLeastDNeg data()[28] 4.200s passed
divGreatestDPos data()[29] 4.297s passed
equivAllRight data()[2] 4.792s passed
divGreatestDNeg data()[30] 4.324s passed
divIncreasingPos data()[31] 4.261s passed
divIncreasingNeg data()[32] 4.225s passed
jdiv_zero data()[33] 4.232s passed
jdivPulloutMinusNum data()[34] 4.321s passed
jdivPulloutMinusDenom data()[35] 4.477s passed
jdiv_uniquePosPos data()[36] 4.252s passed
jdiv_uniquePosNeg data()[37] 4.317s passed
jdiv_uniqueNegPos data()[38] 4.233s passed
jdiv_uniqueNegNeg data()[39] 4.264s passed
irrflConcrete1 data()[3] 4.617s passed
jdivMultDenom1 data()[40] 4.376s passed
jdivMultDenom2 data()[41] 4.378s passed
mod_geZero data()[42] 4.405s passed
mod_lessDenom data()[43] 4.333s passed
jmod_NumPos data()[44] 4.328s passed
jmod_NumNeg data()[45] 4.344s passed
jmod_geZero data()[46] 4.243s passed
jmodNumZero data()[47] 4.167s passed
jmod_pulloutminusNum data()[48] 4.227s passed
jmod_pulloutminusDenom data()[49] 4.268s passed
irrflConcrete2 data()[4] 4.582s passed
jmodUnique1 data()[50] 4.352s passed
jmodUnique2 data()[51] 4.396s passed
intDivRem data()[52] 4.134s passed
jmodjmod data()[53] 4.200s passed
jmodDivisible data()[54] 4.300s passed
jmodDivisibleRep data()[55] 4.226s passed
jdivAddMultDenom data()[56] 4.422s passed
jmodAltZero data()[57] 4.396s passed
jmodAddMultDenomZero data()[58] 4.247s passed
polyDiv_zero data()[59] 4.249s passed
cancel_gtPos data()[5] 4.515s passed
polyMod_ltdivDenom data()[60] 4.162s passed
bsum_empty data()[61] 4.121s passed
bsum_induction_upper data()[62] 4.181s passed
bsum_induction_lower data()[63] 4.079s passed
bsum_num_of_bounds data()[64] 4.144s passed
bsum_num_of_bounds2 data()[65] 4.131s passed
bsum_induction_upper2 data()[66] 4.105s passed
bsum_induction_upper_concrete data()[67] 4.084s passed
bsum_induction_upper_concrete_2 data()[68] 4.122s passed
bsum_induction_upper2_concrete data()[69] 4.137s passed
cancel_gtNeg data()[6] 4.412s passed
bsum_induction_lower_concrete data()[70] 4.197s passed
bsum_induction_lower2 data()[71] 4.243s passed
bsum_induction_lower2_concrete data()[72] 4.231s passed
bsum_positive data()[73] 4.399s passed
bsum_upper_bound data()[74] 4.322s passed
bsum_lower_bound data()[75] 4.202s passed
bsum_positive_lower_bound_element data()[76] 4.187s passed
bsum_sub_same_index data()[77] 4.175s passed
bsum_less_same_index data()[78] 4.226s passed
bsum_equal_except_one_index data()[79] 4.206s passed
moduloIntIsInInt data()[7] 4.497s passed
bsum_num_of_is_max data()[80] 4.306s passed
bsum_num_of_is_max2 data()[81] 4.186s passed
bsum_num_of_is_max3 data()[82] 4.191s passed
bsum_num_of_is_max4 data()[83] 4.231s passed
bsum_num_of_lt_max data()[84] 4.222s passed
bsum_num_of_lt_max2 data()[85] 4.191s passed
bsum_num_of_lt_max3 data()[86] 4.227s passed
bsum_num_of_lt_max4 data()[87] 4.271s passed
bsum_num_of_gt0 data()[88] 4.247s passed
bsum_num_of_gt0_alt data()[89] 4.310s passed
moduloLongIsInLong data()[8] 4.398s passed
bsum_add_concrete data()[90] 4.193s passed
bprod_all_positive data()[91] 4.226s passed
bprod_split data()[92] 4.325s passed
powConcrete0 data()[93] 4.166s passed
powConcrete1 data()[94] 4.220s passed
powSplitFactor data()[95] 4.177s passed
powAdd data()[96] 4.171s passed
powMono data()[97] 4.273s passed
powMonoConcrete data()[98] 4.174s passed
powMonoConcreteRight data()[99] 4.178s passed
moduloShortIsInShort data()[9] 4.453s passed

Standard output

527        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
557        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.99ms 
865        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
888        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)

2089       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2091       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2095       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2095       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3809       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11078      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.21s 
11181      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11231      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.5ns 
11253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11254      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
11262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15000      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.74s 
15003      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16320      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.99ms 
16337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16337      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170ns 
16340      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.57s 
19914      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21107      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21126      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.26ms 
21129      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21129      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.9ns 
21131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24590      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
24590      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
25734      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
25743      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
25746      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
25747      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 487.9ns 
25761      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29169      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
29169      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30320      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
30326      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
30333      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
30334      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 776.31ns 
30335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33706      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
33707      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
34777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
34843      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.43ms 
34847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
34848      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 531.5ns 
34849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38150      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
38151      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
39228      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
39257      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.66ms 
39261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
39261      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 574.1ns 
39263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42628      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
42629      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
43750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
43755      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
43759      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
43759      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 427.7ns 
43761      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47060      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
47061      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
48151      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
48154      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 808.51ns 
48159      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
48159      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.5ns 
48162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51504      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
51505      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
52605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
52608      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 697.41ns 
52612      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
52612      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 488.5ns 
52614      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55886      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
55887      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
56956      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
56959      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 794.2ns 
56962      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
56963      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 415ns 
56964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60242      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
60243      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
61302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
61305      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 611.5ns 
61308      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
61308      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.9ns 
61310      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64556      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
64556      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
65610      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
65675      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.75ms 
65683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
65684      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 696.31ns 
65686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69023      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
69025      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
70062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
70114      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.81ms 
70118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
70118      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.5ns 
70121      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73301      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
73301      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
74365      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
74638      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 262.76ms 
74642      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
74642      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.4ns 
74644      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77961      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
77963      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
79015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
79024      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.37ms 
79028      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
79028      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.5ns 
79030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82265      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
82266      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
83293      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
83297      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
83299      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
83299      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.2ns 
83300      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86439      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
86440      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
87477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
87535      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.66ms 
87538      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
87539      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 439.3ns 
87540      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90769      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
90770      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
91803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
91826      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.7ms 
91828      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
91828      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.4ns 
91829      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95073      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
95073      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
96078      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
96101      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.86ms 
96103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
96103      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.3ns 
96109      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99389      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
99390      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
100486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
100510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.94ms 
100512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
100513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.7ns 
100514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.5s 
104019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
105069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
105093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.65ms 
105096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
105096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.4ns 
105098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
108304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
109353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
109389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.98ms 
109390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
109390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
109392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
112641     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
113699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
113702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
113704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
113704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
113705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
117017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
118047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
118109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.33ms 
118112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
118112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.4ns 
118114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
121325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
122370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
122459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 80.69ms 
122466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
122467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 595.9ns 
122469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
125715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
126800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
126875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.28ms 
126877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
126877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
126878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
130094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
131138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
131157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.26ms 
131162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
131163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.1ns 
131165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
134316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
135341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
135359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.28ms 
135361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
135361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.2ns 
135362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
138594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
139639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
139656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.36ms 
139658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
139658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
139659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
142941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
143969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
143980     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.48ms 
143982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
143982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
143983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
147200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
148231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
148241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ms 
148243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
148244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.6ns 
148245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
151425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
152455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
152466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.14ms 
152468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
152468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.2ns 
152469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
155655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
156693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
156698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
156701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
156701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.4ns 
156702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
159953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
160983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
161019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.08ms 
161021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
161021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.8ns 
161022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
164326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
165373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
165496     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 114.47ms 
165498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
165499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.4ns 
165501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
168695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
169717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
169748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.22ms 
169750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
169750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
169751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
172982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
174023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
174063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.91ms 
174068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
174068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.9ns 
174070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
177298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
178269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
178298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.32ms 
178299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
178300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119ns 
178301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
181525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
182533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
182562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.59ms 
182564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
182565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 894.91ns 
182566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
185809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
186862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
186936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.12ms 
186946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
186946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330ns 
186949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
190250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
191311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
191319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
191323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
191324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.2ns 
191326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
194651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
195719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
195725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
195727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
195727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.8ns 
195728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
199033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
200046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
200058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.08ms 
200059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
200059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
200060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
203322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
204372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
204386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.43ms 
204388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
204388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
204390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
207658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
208702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
208730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.86ms 
208731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
208731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
208732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
211895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
212961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
212973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.8ms 
212974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
212975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98ns 
212975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
216075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
217134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
217140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
217144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
217146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.46ms 
217147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
220370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
221364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
221370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
221371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
221371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
221372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
224560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
225596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
225637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.66ms 
225640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
225640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.6ns 
225641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
228826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
229842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
229988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 135.26ms 
229991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
229991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.2ns 
229993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
233205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
234251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
234383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 121.54ms 
234387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
234388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407ns 
234389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
237494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
238515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
238519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
238522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
238522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.2ns 
238523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
241679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
242664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
242719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.09ms 
242721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
242721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.3ns 
242722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
245926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
246952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
247019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.64ms 
247022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
247022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.7ns 
247023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
250179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
251239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
251245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
251246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
251246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
251248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
254393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
255428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
255666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 225.35ms 
255669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
255669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.4ns 
255670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
258844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
260047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
260063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.58ms 
260066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
260066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.7ns 
260067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
263295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
264299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
264310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.14ms 
264311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
264312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
264312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
267511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
268534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
268559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.75ms 
268560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
268560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
268561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
271687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
272703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
272720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.59ms 
272723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
272723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
272724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
275837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
276835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
276841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
276844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
276855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.27ms 
276856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
280030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
281017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
281023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
281024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
281024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
281025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
284100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
285068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
285102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.27ms 
285104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
285104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
285105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
288207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
289220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
289246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.73ms 
289247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
289247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
289248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
292318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
293350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
293377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.77ms 
293379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
293379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.3ns 
293380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
296493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
297478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
297483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
297484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
297484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.6ns 
297485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
300581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
301560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
301566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
301568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
301568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
301569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
304681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
305680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
305688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
305690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
305690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
305691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
308810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
309819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
309825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
309827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
309827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.1ns 
309828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
312992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
314019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
314022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
314024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
314024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
314025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
317184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
318259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
318265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
318267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
318267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.2ns 
318268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
321463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
322490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
322494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
322498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
322498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
322499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
325756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
326816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
326894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.22ms 
326897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
326897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.1ns 
326898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
330103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
331158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
331217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.82ms 
331219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
331219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
331220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
334376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
335370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
335420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.95ms 
335421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
335421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
335423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
338503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
339527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
339606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.29ms 
339608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
339608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.7ns 
339609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
342751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
343730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
343781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.53ms 
343782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
343782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
343783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
346917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
347926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
348007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.6ms 
348010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
348010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 560.8ns 
348012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
351145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
352166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
352213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.12ms 
352215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
352216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.1ns 
352217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
355441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
356485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
356519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.61ms 
356521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
356521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
356522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
359676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
360658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
360705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.32ms 
360708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
360716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.81ms 
360717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
363890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
364859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
364897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.17ms 
364898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
364898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
364899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
368068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
369082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
369127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.83ms 
369129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
369129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
369130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
372287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
373309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
373350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.09ms 
373352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
373352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
373353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
376484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
377501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
377540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.26ms 
377543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
377543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
377544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
380739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
381729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
381768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.98ms 
381770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
381770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
381771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
384991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
386005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
386039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.9ms 
386041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
386041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
386042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
389216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
390239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
390286     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.22ms 
390288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
390288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
390289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
393506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
394553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
394596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.91ms 
394598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
394598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
394599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
397736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
398778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
398789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.71ms 
398791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
398791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
398792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
401985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
402988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
403015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.15ms 
403017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
403017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
403018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
406285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
407335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
407340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
407341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
407341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
407342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
410496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
411504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
411507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 893.21ns 
411508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
411508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
411509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
414711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
415722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
415726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 949.71ns 
415728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
415728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
415729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
418863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
419894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
419905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.52ms 
419906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
419906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
419907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
423088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
424066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
424075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
424077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
424077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
424078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
427275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
428330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
428348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.88ms 
428364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
428365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 519.2ns 
428366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
431516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
432516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
432522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
432524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
432524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
432525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
435699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
436698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
436701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.8ns 
436702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
436702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
436703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
439834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
440875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
440883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
440884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
440884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
440885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
444040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
445013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
445016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
445018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
445018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
445019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
448157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
449178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
449181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.11ns 
449183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
449183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.2ns 
449184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
452337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
453368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
453371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
453372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
453373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
453373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
456494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
457492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
457498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
457499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
457499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns 
457500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
460601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
461607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
461620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.67ms 
461622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
461622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
461623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
464829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
465831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
465836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms 
465837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
465837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
465838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
468984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
470055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
470067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.22ms 
470069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
470069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.2ns 
470070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
473300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
474349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
474355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
474356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
474356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
474361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
477547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
478555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
478578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.32ms 
478580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
478580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
478581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
481741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
482773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
482778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.08ms 
482779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
482779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
482780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
485949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
486955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
486959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
486960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
486960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
486961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
490136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
491157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
491162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.08ms 
491163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
491163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
491164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
494292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
495312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
495338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.98ms 
495340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
495340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
495340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
498461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
499482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
499488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 823.11ns 
499491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
499491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213.3ns 
499493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
502683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
503697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
503760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.57ms 
503763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
503763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.9ns 
503764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
507069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
508121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
508125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
508126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
508126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
508127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
511317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
512382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
512416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.64ms 
512418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
512418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126ns 
512419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
515618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
516657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
516687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.25ms 
516689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
516689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
516690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
519952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
520949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
520985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.4ms 
520986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
520987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.8ns 
520987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
524245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
525310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
525313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 895.91ns 
525315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
525315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
525316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
528457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
529474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
529482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ms 
529483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
529484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.1ns 
529484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
532662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
533689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
533693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
533694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
533694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
533695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
536879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
537873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
537876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
537878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
537878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
537879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
541043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
542053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
542056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
542058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
542058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
542058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
545224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
546236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
546240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
546246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
546246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 417.1ns 
546247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
549447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
550423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
550427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
550428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
550429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.3ns 
550430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
553564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
554595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
554609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.3ms 
554611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
554611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
554611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
557708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
558728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
558747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.76ms 
558748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
558749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
558749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
561930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
562945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
562974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.78ms 
562976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
562976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
562977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
566169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
567258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
567280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.1ms 
567282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
567282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111ns 
567283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
570479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
571558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
571565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
571567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
571567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
571568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
574814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
575870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
575878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.42ms 
575879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
575880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
575880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
579043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
580124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
580127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 972.81ns 
580128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
580129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
580129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
583365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
584432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
584436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
584437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
584437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns 
584438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
587617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
588701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
588704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
588705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
588706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
588707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
591877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
592923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
592939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.56ms 
592941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
592941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
592942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
596161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
597215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
597221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.93ms 
597222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
597222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
597223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
600305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
601321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
601331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.53ms 
601333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
601333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
601334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
604452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
605476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
605479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
605480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
605480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
605481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
608583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
609624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
609626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 815.4ns 
609628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
609628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
609629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
612722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
613749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
613754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 
613756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
613756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
613757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
616852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
617888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
617892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
617893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
617894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
617894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
621026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
622055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
622062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
622064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
622064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
622065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
625270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
626314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
626318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
626320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
626320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
626320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
629480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
630529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
630537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
630539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
630539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
630540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
633710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
634741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
634745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
634747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
634747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
634748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
637918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
638977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
638995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.51ms 
638997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
638997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
638998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
642152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
643192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
643195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 845.8ns 
643197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
643197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
643197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
646376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
647411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
647421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.05ms 
647422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
647422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
647423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
650572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
651605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
651611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.27ms 
651615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
651615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
651616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
654848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
655893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
655896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
655898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
655898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
655899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
659060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
659060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
660123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
660130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.12ms 
660132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
660132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.5ns 
660132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
663274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
663274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
664290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
664295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
664297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
664297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
664298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
667396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
667397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
668434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
668440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.93ms 
668441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
668441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
668442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
671598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
672605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
672610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
672612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
672612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
672613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
675789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
676823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
676830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
676831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
676831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
676832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
679928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
680972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
680995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.69ms 
680997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
680997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
680998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
684116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
685153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
685181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.21ms 
685183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
685186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
685187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
688463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
688463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
689505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
689520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.53ms 
689522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
689522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
689523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
692773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
692773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
693832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
693849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.17ms 
693851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
693851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109ns 
693852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
697083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
698093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
698167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.76ms 
698169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
698169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
698169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
701353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
702426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
702465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.48ms 
702467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
702467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
702468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
705642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
706686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
706726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.54ms 
706727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
706727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.1ns 
706728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
709831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
710860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
710880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.14ms 
710881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
710881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
710882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
714053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
714053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
715099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
715158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.87ms 
715161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
715161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.6ns 
715162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
718286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
718286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
719317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
719392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.35ms 
719395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
719395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
719396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
722621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
722622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
723674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
723733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.18ms 
723735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
723735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
723736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
726986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
728097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
728165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.43ms 
728167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
728167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
728168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
731406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
732476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
732545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.62ms 
732547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
732547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
732548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
735728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
736765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
736940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 167.04ms 
736942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
736942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
736943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
740101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
740102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
741132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
741143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.95ms 
741145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
741145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
741146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
744300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
744300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
745305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
745317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.39ms 
745319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
745319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
745320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
748469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
749508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
749514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.87ms 
749520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
749520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.5ns 
749521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
752653     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
753724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
753753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.7ms 
753755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
753755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
753756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
756893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
757953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
757970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.11ms 
757972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
757972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
757973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
761159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
761159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
762193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
762198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
762199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
762199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
762200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
765469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
766506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
766533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.65ms 
766535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
766535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
766536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
769667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
769667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
770695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
770723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.71ms 
770724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
770724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
770725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
773941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
775002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
775032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.35ms 
775034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
775034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
775035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
778241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
778241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
779278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
779282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
779284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
779284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
779284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
782441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
782441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
783480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
783485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
783486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
783486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
783487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
786656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
786656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
787776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
787785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.09ms 
787786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
787786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
787787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
790954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
790955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
791985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
791994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 
791995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
791995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
791997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
795155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
795155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
796229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
796344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.06ms 
796345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
796345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
796346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
799513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
799513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
800572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
800615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.23ms 
800617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
800618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.7ns 
800619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
803769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
803769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
804806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
804839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.3ms 
804841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
804842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.4ns 
804842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
808028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
808028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
809061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
809063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 336.5ns 
809065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
809065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
809066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
812271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
813307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
813625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 305.54ms 
813628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
813628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.1ns 
813629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
816789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
816790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
817848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
817925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71ms 
817927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
817927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
817928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
821093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
821093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
822138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
822141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 623.3ns 
822144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
822144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.2ns 
822146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
825373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
825374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
826385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
826387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 491.8ns 
826389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
826389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
826390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
829615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
829615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
830667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
830669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.9ns 
830671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
830671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
830672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
833889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
833889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
834947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
834949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 747.01ns 
834951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
834951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
834952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
838135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
838136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
839194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
839336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 137.84ms 
839338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
839339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 276.1ns 
839340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
842597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
842597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
843642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
843704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.09ms 
843706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
843706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
843707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
846902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
846902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
847982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
847984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 
848019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
848063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
848095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
848104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
848117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
848121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
848122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
848125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
848131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
848134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
848140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
848142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
848383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
848384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
848385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
848387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
848388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
848539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
848541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
848541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
848543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
848545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
848546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
848789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
848791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
848792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
848793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
848794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
848795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
848959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
848961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
848962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
848963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
848964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
848965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
848980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
848981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
848982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
848985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
848986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
848987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
848995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
848996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
848997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
848998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
848999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
849000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
849221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
849222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
849223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
849371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
849373     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)'' 
849376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
849377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
849378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
849379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
849380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
849381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
849387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
849389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
849391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
849391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
849393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
849528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
849533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
849535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
849536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
849537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
849538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
849539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
849691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
849694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
849695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
849697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
849698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
849699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
849699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
849701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
849831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
849834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
849959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
849972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
849981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
849982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
849983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
849985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
849986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
849986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
849987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
849989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
850000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
850006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
850152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
850154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
850155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
850157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
850158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
850159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
850160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
850161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
850246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
850254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
850380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
850383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
850385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
850387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
850388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
850389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
850576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
850582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
850583     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)'' 
850586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
850588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
850589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
850590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
850591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
850605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
850607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
850609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
850609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
850762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
850764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
850765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
850767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
850768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
850769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
850926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
850928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
850929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
850931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
850932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
850932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
850933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
850935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
851058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
851060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
851168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
851170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
851171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
851176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
851181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
851188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
851349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
851351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
851351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
851353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
851366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
851481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
856084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
856086     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)'' 
856096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
856097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
856098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
856101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
856102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
856114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
856118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
856119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
856121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
856122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
856252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
856257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
856259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
856260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
856261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
856262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
856263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
856392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
856394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
856395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
856397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
856398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
856399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
856399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
856401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
856506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
856508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
856610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
856616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
856621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
856623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
856623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
856624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
856637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
856746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
856748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
856748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
856750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
856846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
856857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
856858     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)'' 
856861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
856861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
856862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
856863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
856864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
856877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
856878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
856879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
856880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
856880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
857000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
857002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
857003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
857004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
857005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
857124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
857130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
857131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
857132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
857133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
857133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
857140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
857270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
857272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
857273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
857275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
857277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
857279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
857280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
857282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
857283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
857284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
857285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
857285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
857288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
857289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
857290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
857412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
857413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
857422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
857588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
857696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
857697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
857698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
857700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
857701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
857702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
857702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
857703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
857705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
857820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
857828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
857950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
857951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
857952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
857954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
857954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
857955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
857955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
857956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
857963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
857964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
858080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
858087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
858094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
858225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
858227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
858228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
858229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
858229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
858230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
858230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
858231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
858305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
858307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
858307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
858308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
858309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
858316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
858323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
858479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
858596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
858597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
858598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
858600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
858818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
858933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
858934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
862940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
862948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
862949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
862950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
862950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
863105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
863107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
863108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
863109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
863110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
863250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
867290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
871464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
871470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
871472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
871472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
871473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
871617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
871619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
871620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
871622     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)' ...' 
871624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
873112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
873112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
873113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
876357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
876357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
877414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
877417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
877417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
877425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
877452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
877455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
877465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
877465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
877471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
877472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
877475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
877479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
877479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
877490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
877492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
877492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
877554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
877555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
877556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
877556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
877557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
877646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
877647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
877649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
877650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
877651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
877655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
877656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
877657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
877658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
877659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
877660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
877774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
877775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
877776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
877777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
877779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
877779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
877900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
877901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
877902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
877903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
877904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
877905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
877906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
877907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
877908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
877909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
877909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
877910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
877911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
877912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
877912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
877913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
877914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
877915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
877916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
877919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
877976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
877978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
878065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
878067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
878069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
878071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
878072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
878073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
878144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
878147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
878148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
878150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
878152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
878153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
878154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
878220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
878223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
878227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
878310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
878400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
878401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.5ns 
878402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
881723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
881723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
882808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
882856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.46ms