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

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

tests
0

failures
0

ignored
14m47.94s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.325s passed
powPositiveConcrete data()[101] 4.444s passed
powGeq1Concrete data()[102] 4.366s passed
pow2InIntLower data()[103] 4.699s passed
pow2InIntUpper data()[104] 4.612s passed
logSelfConcrete data()[105] 4.242s passed
log1Concrete data()[106] 4.264s passed
logProduct data()[107] 4.178s passed
logTimesBaseConcrete data()[108] 4.242s passed
logProdIdentity data()[109] 4.374s passed
moduloByteIsInByte data()[10] 4.186s passed
logProdIdentityConcrete data()[110] 4.171s passed
logPowIdentity data()[111] 4.093s passed
logPowIdentityConcrete data()[112] 4.136s passed
logPositive data()[113] 4.395s passed
logPositiveConcrete data()[114] 4.449s passed
logMono data()[115] 4.531s passed
logMonoConcrete data()[116] 4.445s passed
powLogLess data()[117] 4.494s passed
powLogMore2 data()[118] 4.350s passed
logLessThanPow data()[119] 4.446s passed
moduloCharIsInChar data()[11] 4.125s passed
logLessThanPowConcrete data()[120] 4.379s passed
logSqueeze data()[121] 4.389s passed
ifthenelse_equals data()[122] 4.358s passed
ifthenelse_equals_1 data()[123] 4.592s passed
ifthenelse_equals_2 data()[124] 4.603s passed
disjointWithSingleton1 data()[125] 4.382s passed
disjointWithSingleton2 data()[126] 4.377s passed
disjointArrayRanges data()[127] 4.381s passed
disjointArrayRangeAllFields1 data()[128] 4.318s passed
disjointArrayRangeAllFields2 data()[129] 4.351s passed
div_unique1 data()[12] 4.198s passed
seqSelfDefinition data()[130] 4.365s passed
seqOutsideValue data()[131] 4.253s passed
castedGetAny data()[132] 4.432s passed
seqGetAlphaCast data()[133] 4.207s passed
getOfSeqSingleton data()[134] 4.101s passed
getOfSeqSingletonConcrete data()[135] 4.042s passed
getOfSeqConcat data()[136] 4.337s passed
getOfSeqSub data()[137] 4.221s passed
getOfSeqReverse data()[138] 4.183s passed
lenOfSeqEmpty data()[139] 3.904s passed
div_unique2 data()[13] 4.555s passed
lenOfSeqSingleton data()[140] 3.897s passed
lenOfSeqConcat data()[141] 3.921s passed
lenOfSeqSub data()[142] 3.824s passed
lenOfSeqReverse data()[143] 3.854s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.091s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.984s passed
getOfSeqSingletonEQ data()[146] 4.125s passed
getOfSeqConcatEQ data()[147] 4.088s passed
getOfSeqSubEQ data()[148] 4.213s passed
getOfSeqReverseEQ data()[149] 3.996s passed
div_exists data()[14] 4.750s passed
lenOfSeqEmptyEQ data()[150] 4.167s passed
lenOfSeqSingletonEQ data()[151] 4.041s passed
lenOfSeqConcatEQ data()[152] 4.164s passed
lenOfSeqSubEQ data()[153] 4.151s passed
lenOfSeqReverseEQ data()[154] 4.183s passed
getOfSeqDefEQ data()[155] 4.153s passed
lenOfSeqDefEQ data()[156] 4.227s passed
seqConcatWithSeqEmpty1 data()[157] 4.473s passed
seqConcatWithSeqEmpty2 data()[158] 4.369s passed
seqReverseOfSeqEmpty data()[159] 4.668s passed
div_one data()[15] 4.556s passed
subSeqComplete data()[160] 4.342s passed
subSeqTailR data()[161] 4.428s passed
subSeqTailL data()[162] 4.508s passed
subSeqTailEQR data()[163] 4.269s passed
subSeqTailEQL data()[164] 4.283s passed
seqDef_split data()[165] 4.518s passed
seqDef_induction_upper data()[166] 4.427s passed
seqDef_induction_upper_concrete data()[167] 4.543s passed
seqDef_induction_lower data()[168] 4.582s passed
seqDef_induction_lower_concrete data()[169] 4.326s passed
jdiv_one data()[16] 4.457s passed
seqDef_split_in_three data()[170] 4.297s passed
seqDef_empty data()[171] 4.265s passed
seqDef_one_summand data()[172] 4.054s passed
seqDef_lower_equals_upper data()[173] 4.151s passed
seqDefOfSeq data()[174] 4.014s passed
seqSelfDefinitionEQ2 data()[175] 4.312s passed
indexOfSeqSingleton data()[176] 4.021s passed
indexOfSeqConcatFirst data()[177] 3.935s passed
indexOfSeqConcatSecond data()[178] 4.226s passed
indexOfSeqSub data()[179] 4.277s passed
div_zero data()[17] 4.601s passed
lenOfArray2seq data()[180] 4.481s passed
getAnyOfArray2seq data()[181] 4.237s passed
getOfArray2seq data()[182] 4.543s passed
getAnyOfNPermInv data()[183] 4.356s passed
seqNPermRange data()[184] 4.518s passed
seqPermTrans data()[185] 4.426s passed
seqPermRefl data()[186] 4.513s passed
seqPermSplit data()[187] 4.314s passed
seqNPermRight data()[188] 5.177s passed
seqPermFromSwap data()[189] 5.130s passed
divResZero1 data()[18] 4.500s passed
seqPermTransAlt0 data()[190] 4.467s passed
seqPermTransAlt1 data()[191] 4.668s passed
seqPermTransAlt2 data()[192] 4.645s passed
seqPermTransAlt3 data()[193] 4.673s passed
seqPermForall data()[194] 4.396s passed
seqPermExists data()[195] 4.296s passed
schiffl_lemma_2 data()[196] 33.243s passed
schiffl_thm_1 data()[197] 5.832s passed
eqSameSeq data()[198] 4.547s passed
divResZero2 data()[19] 4.096s passed
eqTermCut data()[1] 4.897s passed
divResOne1 data()[20] 4.345s passed
divResOne2 data()[21] 4.022s passed
div_cancel1 data()[22] 4.381s passed
div_cancel2 data()[23] 4.072s passed
divAddMultDenom data()[24] 4.440s passed
divMinus data()[25] 4.161s passed
divMinusDenom data()[26] 4.361s passed
divLeastDPos data()[27] 4.370s passed
divLeastDNeg data()[28] 4.393s passed
divGreatestDPos data()[29] 4.434s passed
equivAllRight data()[2] 4.482s passed
divGreatestDNeg data()[30] 4.368s passed
divIncreasingPos data()[31] 4.231s passed
divIncreasingNeg data()[32] 4.006s passed
jdiv_zero data()[33] 4.492s passed
jdivPulloutMinusNum data()[34] 4.425s passed
jdivPulloutMinusDenom data()[35] 4.460s passed
jdiv_uniquePosPos data()[36] 4.596s passed
jdiv_uniquePosNeg data()[37] 5.115s passed
jdiv_uniqueNegPos data()[38] 4.872s passed
jdiv_uniqueNegNeg data()[39] 4.402s passed
irrflConcrete1 data()[3] 4.643s passed
jdivMultDenom1 data()[40] 4.272s passed
jdivMultDenom2 data()[41] 4.362s passed
mod_geZero data()[42] 4.287s passed
mod_lessDenom data()[43] 4.251s passed
jmod_NumPos data()[44] 4.332s passed
jmod_NumNeg data()[45] 4.220s passed
jmod_geZero data()[46] 4.287s passed
jmodNumZero data()[47] 4.236s passed
jmod_pulloutminusNum data()[48] 4.492s passed
jmod_pulloutminusDenom data()[49] 4.242s passed
irrflConcrete2 data()[4] 4.452s passed
jmodUnique1 data()[50] 4.482s passed
jmodUnique2 data()[51] 4.462s passed
intDivRem data()[52] 4.180s passed
jmodjmod data()[53] 4.290s passed
jmodDivisible data()[54] 4.275s passed
jmodDivisibleRep data()[55] 4.215s passed
jdivAddMultDenom data()[56] 4.369s passed
jmodAltZero data()[57] 4.173s passed
jmodAddMultDenomZero data()[58] 4.532s passed
polyDiv_zero data()[59] 4.611s passed
cancel_gtPos data()[5] 4.390s passed
polyMod_ltdivDenom data()[60] 4.261s passed
bsum_empty data()[61] 4.813s passed
bsum_induction_upper data()[62] 4.379s passed
bsum_induction_lower data()[63] 4.303s passed
bsum_num_of_bounds data()[64] 4.096s passed
bsum_num_of_bounds2 data()[65] 4.162s passed
bsum_induction_upper2 data()[66] 4.104s passed
bsum_induction_upper_concrete data()[67] 4.132s passed
bsum_induction_upper_concrete_2 data()[68] 4.116s passed
bsum_induction_upper2_concrete data()[69] 4.118s passed
cancel_gtNeg data()[6] 4.245s passed
bsum_induction_lower_concrete data()[70] 4.115s passed
bsum_induction_lower2 data()[71] 4.181s passed
bsum_induction_lower2_concrete data()[72] 4.219s passed
bsum_positive data()[73] 4.301s passed
bsum_upper_bound data()[74] 4.245s passed
bsum_lower_bound data()[75] 4.294s passed
bsum_positive_lower_bound_element data()[76] 4.232s passed
bsum_sub_same_index data()[77] 4.224s passed
bsum_less_same_index data()[78] 4.208s passed
bsum_equal_except_one_index data()[79] 4.220s passed
moduloIntIsInInt data()[7] 4.298s passed
bsum_num_of_is_max data()[80] 4.153s passed
bsum_num_of_is_max2 data()[81] 4.190s passed
bsum_num_of_is_max3 data()[82] 4.163s passed
bsum_num_of_is_max4 data()[83] 4.151s passed
bsum_num_of_lt_max data()[84] 4.274s passed
bsum_num_of_lt_max2 data()[85] 4.223s passed
bsum_num_of_lt_max3 data()[86] 4.289s passed
bsum_num_of_lt_max4 data()[87] 4.348s passed
bsum_num_of_gt0 data()[88] 4.480s passed
bsum_num_of_gt0_alt data()[89] 4.416s passed
moduloLongIsInLong data()[8] 4.122s passed
bsum_add_concrete data()[90] 4.363s passed
bprod_all_positive data()[91] 4.262s passed
bprod_split data()[92] 4.279s passed
powConcrete0 data()[93] 4.250s passed
powConcrete1 data()[94] 4.467s passed
powSplitFactor data()[95] 4.370s passed
powAdd data()[96] 4.365s passed
powMono data()[97] 4.639s passed
powMonoConcrete data()[98] 4.415s passed
powMonoConcreteRight data()[99] 4.449s passed
moduloShortIsInShort data()[9] 4.339s passed

Standard output

456        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
486        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.96ms 
741        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
761        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)

1888       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1892       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1896       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1897       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4103       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10636      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.89s 
10710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10753      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.9ns 
10771      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10772      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 559.61ns 
10777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14420      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.64s 
14424      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
15628      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
15657      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.18ms 
15675      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
15676      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 583.5ns 
15678      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19013      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
19014      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
20119      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
20149      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.04ms 
20155      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
20155      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 451.4ns 
20162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23641      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.48s 
23641      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
24785      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
24795      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
24799      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
24800      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.6ns 
24805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28127      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
28127      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
29229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
29249      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ms 
29256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
29256      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 428.1ns 
29261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32570      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
32571      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
33575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
33640      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.74ms 
33645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
33645      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 450.8ns 
33647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36855      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
36856      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
37856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
37886      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.11ms 
37889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
37889      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.7ns 
37890      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41141      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
41141      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
42180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
42185      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
42188      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
42188      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.8ns 
42190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45254      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
45255      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
46301      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
46307      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.11ns 
46311      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
46311      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.5ns 
46312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49563      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
49563      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
50644      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
50648      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 759.41ns 
50652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
50652      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 450.7ns 
50655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53839      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
53840      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
54832      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
54835      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 750.31ns 
54838      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
54838      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.3ns 
54840      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57934      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
57935      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
58956      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
58959      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 692.51ns 
58971      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
58972      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.4ns 
58973      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
62121      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
63108      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
63166      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.54ms 
63171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
63172      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 512.9ns 
63173      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66622      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.45s 
66623      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
67665      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
67720      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.58ms 
67727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
67728      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 673.91ns 
67730      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71052      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
71053      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
72203      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
72472      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 252.88ms 
72477      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
72477      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 684.11ns 
72479      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75887      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
75887      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
77022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
77030      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
77033      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
77034      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 415ns 
77035      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80288      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
80290      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
81464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
81488      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
81491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
81492      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 596.5ns 
81495      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84907      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
84908      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
85995      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
86089      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.69ms 
86091      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
86092      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.6ns 
86093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89535      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
89535      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
90567      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
90590      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.25ms 
90592      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
90592      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
90593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93685      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
93685      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
94658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
94685      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.07ms 
94689      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
94690      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 909.21ns 
94695      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98025      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
98026      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
99007      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
99032      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.85ms 
99035      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
99036      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 873.11ns 
99037      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
102055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
103031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
103054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.44ms 
103057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
103057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 549.3ns 
103059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
106410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
107398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
107435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.96ms 
107437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
107437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.4ns 
107438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
110464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
111503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
111507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
111510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
111510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.6ns 
111512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
114849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
115881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
115947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.74ms 
115950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
115950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.9ns 
115952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
119043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
120020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
120107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 79.34ms 
120111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
120112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.7ns 
120113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
123311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
124375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
124469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.54ms 
124473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
124474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 454.7ns 
124475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
127776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
128829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
128840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.31ms 
128842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
128842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.8ns 
128843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
132094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
133213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
133233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.84ms 
133235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
133235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.7ns 
133236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
136561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
137649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
137666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.94ms 
137669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
137670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.1ns 
137671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
140953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
142024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
142035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.44ms 
142037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
142037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.1ns 
142038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
145270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
146251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
146265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.72ms 
146267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
146267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
146269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
149317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
150262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
150272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.24ms 
150275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
150275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.4ns 
150276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
153690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
154759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
154764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
154766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
154767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.6ns 
154768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
158065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
159166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
159189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.9ms 
159191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
159192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.1ns 
159193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
162515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
163567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
163649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.67ms 
163651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
163651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
163652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.56s 
167208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
168214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
168244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.29ms 
168248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
168249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 447ns 
168250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.72s 
171968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
173309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
173358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.4ms 
173365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
173366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 523.9ns 
173368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.77s 
177134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
178206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
178234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.15ms 
178235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
178235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112ns 
178236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
181489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
182610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
182636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.79ms 
182637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
182638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.4ns 
182639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
185810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
186840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
186908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.91ms 
186910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
186910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222ns 
186911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
190245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
191263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
191270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.47ms 
191272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
191272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
191273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
194512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
195550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
195556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
195559     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
195560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.6ns 
195561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
198749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
199796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
199808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.62ms 
199810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
199810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.1ns 
199811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
203091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
204123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
204140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.91ms 
204142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
204142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.2ns 
204143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
207362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
208332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
208360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.96ms 
208362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
208362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.6ns 
208363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
211622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
212635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
212646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.77ms 
212648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
212649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.4ns 
212650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
215893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
216878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
216882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
216884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
216884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.7ns 
216885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
220300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
221367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
221374     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.98ms 
221382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
221382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.1ns 
221384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
224590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
225615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
225621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
225623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
225623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
225624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
228879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
229971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
230102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 120.81ms 
230105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
230106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 500.31ns 
230108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
233384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
234407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
234564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 141.96ms 
234567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
234568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.9ns 
234569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
237732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
238740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
238745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
238750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
238750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.1ns 
238751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
241946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
242973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
243037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.16ms 
243039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
243040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 756.11ns 
243041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
246269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
247266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
247311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.18ms 
247314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
247314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.1ns 
247315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
250493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
251523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
251527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
251529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
251529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.2ns 
251531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
254680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
255667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
255895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 214.14ms 
255899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
255899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.8ns 
255900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
259068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
260052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
260069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.41ms 
260071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
260071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
260072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
263449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
264589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
264601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.43ms 
264603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
264603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
264604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
268066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
269170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
269205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.41ms 
269214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
269214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107ns 
269215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
272466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
273454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
273472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.16ms 
273475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
273475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
273476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.66s 
277132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
278280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
278285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
278288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
278288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.3ns 
278289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
281584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
282658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
282665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.56ms 
282666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
282667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
282667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
285833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
286931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
286968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.03ms 
286970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
286970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
286971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
290036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
291035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
291064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.92ms 
291066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
291066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.6ns 
291067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
294199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
295202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
295226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.75ms 
295227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
295228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
295228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
298313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
299325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
299330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
299332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
299332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
299333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
302438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
303456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
303462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
303464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
303464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
303465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
306554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
307570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
307578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.98ms 
307580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
307580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
307581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
310707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
311691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
311696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
311698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
311699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.2ns 
311700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
314819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
315808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
315811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
315813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
315813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
315814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
318987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
319986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
319992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
319994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
319994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
319995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
323209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
324207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
324211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
324212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
324212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
324213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
327387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
328424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
328511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.1ms 
328515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
328515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.5ns 
328516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
331618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
332676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
332757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.11ms 
332761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
332761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.7ns 
332762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
335990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
337001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
337053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.72ms 
337056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
337056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.2ns 
337057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
340211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
341205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
341285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.26ms 
341288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
341288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.5ns 
341289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
344375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
345447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
345509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.97ms 
345511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
345511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
345512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
348607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
349628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
349717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.55ms 
349719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
349719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.5ns 
349720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
352843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
353886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
353937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.73ms 
353940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
353940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
353941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
357053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
358057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
358091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.73ms 
358092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
358092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
358093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
361271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
362239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
362280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.74ms 
362281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
362282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
362282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
365428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
366409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
366443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.81ms 
366445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
366445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
366446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
369593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
370549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
370594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.4ms 
370595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
370595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
370596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
373782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
374822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
374868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.08ms 
374870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
374870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
374871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
378033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
379049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
379091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.12ms 
379093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
379094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.3ns 
379095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
382289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
383330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
383377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.95ms 
383383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
383384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 717.21ns 
383385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
386664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
387694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
387729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.54ms 
387731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
387731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
387732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
390922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
392170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
392209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.81ms 
392211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
392211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.4ns 
392212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.33s 
395543     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
396582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
396625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.49ms 
396627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
396627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
396628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
399895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
400975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
400988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ms 
400989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
400989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
400991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
404208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
405220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
405250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.38ms 
405252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
405252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
405253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
408511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
409523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
409529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.48ms 
409530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
409530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
409531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
412813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
413777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
413780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 884.01ns 
413781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
413781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
413782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
417141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
418243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
418246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
418248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
418248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
418248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
421585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
422599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
422616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.34ms 
422618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
422618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.9ns 
422619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
425940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
426970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
426981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.66ms 
426983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
426983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
426985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
430452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
431593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
431620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.97ms 
431625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
431626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.2ns 
431627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
434926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
436030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
436035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.81ms 
436037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
436037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
436038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
439419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
440481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
440484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 824.71ns 
440486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
440486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
440487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
443716     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
444800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
444810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
444811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
444811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
444812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
448166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
449250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
449253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
449255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
449255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
449256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
452512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
453613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
453618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
453623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
453623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.6ns 
453624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.51s 
457134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
458317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
458320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 986.41ns 
458322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
458322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
458323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.49s 
461811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
462926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
462932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.18ms 
462933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
462933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
462934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
466135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
467161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
467174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.35ms 
467176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
467176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.2ns 
467177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
470381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
471431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
471438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.61ms 
471440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
471440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.9ns 
471441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
474639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
475606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
475617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.63ms 
475619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
475619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
475620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
478795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
479851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
479858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.63ms 
479860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
479860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
479861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
483100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
484209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
484232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.92ms 
484234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
484234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns 
484234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
487400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
488398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
488403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
488405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
488405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
488405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
491518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
492493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
492497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
492498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
492498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
492499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
495610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
496627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
496633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.91ms 
496634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
496634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
496635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
499914     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
500995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
501027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.91ms 
501029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
501029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.2ns 
501030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
504415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
505468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
505475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 775.01ns 
505478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
505478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
505479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
508800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
509936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
510007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.35ms 
510009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
510009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
510010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
513371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
514444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
514451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
514456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
514456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.9ns 
514458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.32s 
517775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
518913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
518947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.53ms 
518949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
518949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
518950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
522195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
523262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
523297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.81ms 
523299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
523299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
523300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
526615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
527691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
527742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.63ms 
527745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
527745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
527746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
531106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
532119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
532122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 844.51ns 
532124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
532124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
532125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.34s 
535470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
536503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
536511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
536513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
536513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
536514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
539810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
540863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
540868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
540871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
540871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
540872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.54s 
544416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
545457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
545461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
545462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
545463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
545463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.44s 
548904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
550060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
550064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
550066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
550066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.6ns 
550067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
553360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
554441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
554446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
554448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
554448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
554449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
557645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
558818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
558823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
558826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
558826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119ns 
558827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
562105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
563188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
563203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.14ms 
563205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
563205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
563206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
566470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
567501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
567521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.55ms 
567523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
567524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
567524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
570807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
571852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
571872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.86ms 
571876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
571876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.8ns 
571877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
575165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
576220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
576238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.63ms 
576240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
576240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
576241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
579408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
580485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
580491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
580493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
580493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
580494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.31s 
583808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
584914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
584923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.47ms 
584925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
584925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
584926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.18s 
588101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
589127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
589130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 935.61ns 
589132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
589132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
589133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
592208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
593227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
593231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
593233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
593233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
593234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
596297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
597269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
597273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
597274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
597274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
597275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
600496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
601592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
601610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.24ms 
601612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
601612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
601613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
604775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
605824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
605831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.12ms 
605833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
605834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 500.31ns 
605835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
609010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
610005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
610015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.33ms 
610016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
610016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
610017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
612965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
613916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
613919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 853.01ns 
613920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
613920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
613921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
616870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
617813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
617815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.01ns 
617817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
617817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
617817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
620731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
621731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
621737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
621738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
621738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
621739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
624601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
625556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
625560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
625562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
625562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
625562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
628390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
629410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
629414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
629416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
629416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
629417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
632504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
633501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
633505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
633506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
633506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
633507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
636486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
636486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
637482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
637490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
637491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
637491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
637492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
640569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
641610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
641614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
641615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
641615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
641616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
644658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
645685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
645702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.14ms 
645703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
645703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
645704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
648927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
649912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
649915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 969.31ns 
649917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
649917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
649917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
652843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
653901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
653911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.44ms 
653913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
653913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
653914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
657046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
658075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
658078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
658080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
658080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
658080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
661051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
662116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
662120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
662121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
662121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
662122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
665248     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
666276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
666283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.98ms 
666285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
666285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
666286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
669369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
670430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
670434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
670436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
670436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
670437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
673607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
674612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
674617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
674619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
674619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
674619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
677711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
678765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
678770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.32ms 
678774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
678774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
678775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
681978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
682992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
682999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
683001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
683001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.4ns 
683002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
686281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
687446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
687472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.28ms 
687473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
687473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
687474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
690762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
690763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
691818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
691841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.29ms 
691843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
691843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.4ns 
691844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
695316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.47s 
695316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
696494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
696509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.21ms 
696511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
696511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
696512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
699799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
699799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
700835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
700851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.56ms 
700853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
700853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
700854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
704084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.23s 
704084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
705234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
705279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.53ms 
705281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
705281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.5ns 
705282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
708667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
709748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
709787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.85ms 
709789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
709789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
709790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
712960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
713987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
714056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.67ms 
714058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
714058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
714058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
717260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
718318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
718339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.57ms 
718341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
718341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
718342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.37s 
721711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
722804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
722857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.01ms 
722858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
722858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
722859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
726131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.27s 
726131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
727209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
727284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.95ms 
727286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
727286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
727287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
730645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
730646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
731770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
731827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.71ms 
731829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
731829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.1ns 
731830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.36s 
735186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
736334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
736408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.2ms 
736411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
736411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.6ns 
736412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
739613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
740668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
740735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.47ms 
740737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
740737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
740738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
743809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
743810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
744843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
745032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 179.59ms 
745035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
745035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
745036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
748235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
748235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
749287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
749298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.72ms 
749299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
749299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
749300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
752381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
752381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
753340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
753351     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.61ms 
753353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
753353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
753354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
756402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
756402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
757495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
757502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.45ms 
757504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
757504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
757505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
760472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
760473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
761488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
761517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.48ms 
761518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
761518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
761519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
764774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
764774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
765812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
765828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.52ms 
765830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
765830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
765831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
768878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
768879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
769845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
769850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
769851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
769851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
769852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
772785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
772785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
773761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
773784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.6ms 
773786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
773786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
773787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
776935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
777984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
778010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.43ms 
778012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
778012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
778013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
781173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
781174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
782253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
782287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.99ms 
782290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
782290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.9ns 
782291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
785704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.41s 
785704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
786764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
786768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
786770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
786770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114ns 
786771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
789843     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
791000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
791005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
791007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
791007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
791008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
794426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
794426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
795539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
795548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.02ms 
795550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
795550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.6ns 
795551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
798828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.28s 
798828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
799895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
799904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.83ms 
799906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
799906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
799907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
803193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
803193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
804301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
804421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.12ms 
804424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
804425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 890.61ns 
804426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
807724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
807724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
808806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
808848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.74ms 
808850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
808851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.6ns 
808851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
812233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
812233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
813327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
813361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.86ms 
813363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
813364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.7ns 
813364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
816625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.26s 
816625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
817672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
817675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 503.2ns 
817677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
817677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
817682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
821408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.73s 
821409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
822475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
822851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 362.38ms 
822854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
822855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.3ns 
822856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
826613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s 
826613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
827862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
827983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 110.04ms 
827984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
827985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
827985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
831361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.38s 
831361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
832448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
832450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 504ns 
832452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
832452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
832452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
835873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
835873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
837115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
837118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.71ns 
837120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
837120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85ns 
837121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
840584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.46s 
840585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
841760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
841763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 642.21ns 
841765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
841765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
841766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
845288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.52s 
845288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
846433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
846435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 734.21ns 
846437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
846437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
846438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
849651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
849651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
850701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
850810     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
850831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 127.28ms 
850834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
850835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.9ns 
850836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
853996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
853996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
855060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
855128     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
855129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.97ms 
855131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
855131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
855138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
858325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
858326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
859367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
859370     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 
859409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
859493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
859516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
859522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
859535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
859540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
859541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
859548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
859553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
859555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
859558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
859560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
859855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
859858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
859860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
859862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
859863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
860056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
860057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
860058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
860061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
860062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
860063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
860282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
860285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
860286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
860286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
860287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
860289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
860467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
860469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
860470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
860471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
860472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
860473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
860483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
860485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
860489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
860492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
860493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
860495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
860504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
860506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
860507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
860508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
860510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
860511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
860692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
860693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
860695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
860867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
860870     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)'' 
860874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
860875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
860877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
860878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
860879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
860880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
860885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
860889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
860891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
860891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
860893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
861060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
861065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
861068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
861069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
861069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
861071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
861073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
861315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
861317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
861318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
861321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
861322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
861323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
861324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
861325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
861487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
861489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
861643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
861650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
861658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
861660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
861661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
861663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
861664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
861665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
861665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
861668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
861681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
861689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
861882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
861884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
861885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
861887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
861888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
861889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
861889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
861891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
861983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
861993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
862149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
862152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
862154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
862156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
862157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
862159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
862346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
862351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
862353     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)'' 
862360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
862363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
862364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
862365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
862366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
862379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
862387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
862389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
862390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
862514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
862515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
862517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
862521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
862523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
862524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
862692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
862694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
862695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
862697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
862697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
862698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
862698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
862700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
862817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
862819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
862946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
862946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
862947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
862953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
862959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
862966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
863209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
863212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
863213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
863215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
863231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
863341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
868307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
868309     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)'' 
868316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
868317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
868318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
868319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
868320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
868332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
868334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
868336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
868337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
868338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
868511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
868523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
868527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
868529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
868532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
868537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
868539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
868709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
868714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
868715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
868721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
868723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
868724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
868725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
868726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
868843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
868846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
868965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
868972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
868980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
868981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
868983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
868984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
869001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
869117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
869118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
869119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
869121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
869256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
869271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
869273     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)'' 
869277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
869278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
869281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
869287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
869288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
869315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
869318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
869320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
869322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
869331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
869543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
869545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
869546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
869547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
869548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
869692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
869698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
869699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
869702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
869703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
869704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
869705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
869864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
869867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
869868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
869870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
869870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
869871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
869874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
869880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
869883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
869884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
869887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
869888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
869889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
869890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
869892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
870024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
870026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
870035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
870164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
870306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
870309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
870310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
870311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
870313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
870314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
870314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
870315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
870316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
870436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
870447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
870614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
870616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
870618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
870620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
870621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
870621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
870622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
870624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
870634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
870636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
870766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
870774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
870784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
870967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
870969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
870971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
870973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
870974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
870974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
870975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
870976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
871072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
871074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
871075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
871076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
871077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
871089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
871104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
871281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
871413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
871415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
871416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
871418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
871704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
871850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
871852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
876627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
876638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
876640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
876641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
876642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
876835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
876837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
876840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
876841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
876842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
876983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
881334     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
886311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
886317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
886319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
886320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
886321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
886477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
886479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
886480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
886482     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)' ...' 
886484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
888375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
888375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112ns 
888376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
891972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.6s 
891972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
893134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
893136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ns 
893136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
893144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
893159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
893162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
893164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
893165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
893170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
893172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
893176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
893180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
893181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
893196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
893199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
893200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
893286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
893288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
893288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
893289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
893290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
893382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
893383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
893387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
893388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
893389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
893394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
893395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
893396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
893397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
893399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
893399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
893510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
893511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
893512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
893513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
893515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
893516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
893635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
893636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
893638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
893639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
893640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
893642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
893642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
893643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
893644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
893645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
893645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
893647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
893648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
893649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
893649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
893650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
893651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
893653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
893655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
893662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
893720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
893722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
893827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
893829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
893831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
893833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
893835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
893836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
893930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
893935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
893938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
893941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
893944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
893945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
893947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
894039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
894044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
894049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
894128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
894205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
894206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.4ns 
894207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
897556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.35s 
897557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
898701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
898751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.41ms