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

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

tests
0

failures
0

ignored
11m56.25s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.456s passed
powPositiveConcrete data()[101] 3.443s passed
powGeq1Concrete data()[102] 3.480s passed
pow2InIntLower data()[103] 3.455s passed
pow2InIntUpper data()[104] 3.451s passed
logSelfConcrete data()[105] 3.459s passed
log1Concrete data()[106] 3.472s passed
logProduct data()[107] 3.480s passed
logTimesBaseConcrete data()[108] 3.458s passed
logProdIdentity data()[109] 3.467s passed
moduloByteIsInByte data()[10] 3.561s passed
logProdIdentityConcrete data()[110] 3.467s passed
logPowIdentity data()[111] 3.458s passed
logPowIdentityConcrete data()[112] 3.460s passed
logPositive data()[113] 3.511s passed
logPositiveConcrete data()[114] 3.472s passed
logMono data()[115] 3.480s passed
logMonoConcrete data()[116] 3.490s passed
powLogLess data()[117] 3.491s passed
powLogMore2 data()[118] 3.515s passed
logLessThanPow data()[119] 3.511s passed
moduloCharIsInChar data()[11] 3.524s passed
logLessThanPowConcrete data()[120] 3.451s passed
logSqueeze data()[121] 3.459s passed
ifthenelse_equals data()[122] 3.486s passed
ifthenelse_equals_1 data()[123] 3.452s passed
ifthenelse_equals_2 data()[124] 3.441s passed
disjointWithSingleton1 data()[125] 3.480s passed
disjointWithSingleton2 data()[126] 3.470s passed
disjointArrayRanges data()[127] 3.455s passed
disjointArrayRangeAllFields1 data()[128] 3.481s passed
disjointArrayRangeAllFields2 data()[129] 3.471s passed
div_unique1 data()[12] 3.601s passed
seqSelfDefinition data()[130] 3.470s passed
seqOutsideValue data()[131] 3.507s passed
castedGetAny data()[132] 3.463s passed
seqGetAlphaCast data()[133] 3.455s passed
getOfSeqSingleton data()[134] 3.518s passed
getOfSeqSingletonConcrete data()[135] 3.480s passed
getOfSeqConcat data()[136] 3.535s passed
getOfSeqSub data()[137] 3.506s passed
getOfSeqReverse data()[138] 3.472s passed
lenOfSeqEmpty data()[139] 3.522s passed
div_unique2 data()[13] 3.565s passed
lenOfSeqSingleton data()[140] 3.499s passed
lenOfSeqConcat data()[141] 3.482s passed
lenOfSeqSub data()[142] 3.449s passed
lenOfSeqReverse data()[143] 3.474s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.462s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.479s passed
getOfSeqSingletonEQ data()[146] 3.492s passed
getOfSeqConcatEQ data()[147] 3.514s passed
getOfSeqSubEQ data()[148] 3.473s passed
getOfSeqReverseEQ data()[149] 3.483s passed
div_exists data()[14] 3.712s passed
lenOfSeqEmptyEQ data()[150] 3.455s passed
lenOfSeqSingletonEQ data()[151] 3.497s passed
lenOfSeqConcatEQ data()[152] 3.469s passed
lenOfSeqSubEQ data()[153] 3.477s passed
lenOfSeqReverseEQ data()[154] 3.498s passed
getOfSeqDefEQ data()[155] 3.473s passed
lenOfSeqDefEQ data()[156] 3.501s passed
seqConcatWithSeqEmpty1 data()[157] 3.507s passed
seqConcatWithSeqEmpty2 data()[158] 3.457s passed
seqReverseOfSeqEmpty data()[159] 3.487s passed
div_one data()[15] 3.530s passed
subSeqComplete data()[160] 3.484s passed
subSeqTailR data()[161] 3.463s passed
subSeqTailL data()[162] 3.488s passed
subSeqTailEQR data()[163] 3.509s passed
subSeqTailEQL data()[164] 3.462s passed
seqDef_split data()[165] 3.499s passed
seqDef_induction_upper data()[166] 3.524s passed
seqDef_induction_upper_concrete data()[167] 3.509s passed
seqDef_induction_lower data()[168] 3.539s passed
seqDef_induction_lower_concrete data()[169] 3.508s passed
jdiv_one data()[16] 3.503s passed
seqDef_split_in_three data()[170] 3.601s passed
seqDef_empty data()[171] 3.488s passed
seqDef_one_summand data()[172] 3.504s passed
seqDef_lower_equals_upper data()[173] 3.521s passed
seqDefOfSeq data()[174] 3.502s passed
seqSelfDefinitionEQ2 data()[175] 3.467s passed
indexOfSeqSingleton data()[176] 3.482s passed
indexOfSeqConcatFirst data()[177] 3.508s passed
indexOfSeqConcatSecond data()[178] 3.495s passed
indexOfSeqSub data()[179] 3.568s passed
div_zero data()[17] 3.584s passed
lenOfArray2seq data()[180] 3.507s passed
getAnyOfArray2seq data()[181] 3.490s passed
getOfArray2seq data()[182] 3.492s passed
getAnyOfNPermInv data()[183] 3.500s passed
seqNPermRange data()[184] 3.526s passed
seqPermTrans data()[185] 3.534s passed
seqPermRefl data()[186] 3.501s passed
seqPermSplit data()[187] 3.475s passed
seqNPermRight data()[188] 3.670s passed
seqPermFromSwap data()[189] 3.543s passed
divResZero1 data()[18] 3.540s passed
seqPermTransAlt0 data()[190] 3.514s passed
seqPermTransAlt1 data()[191] 3.467s passed
seqPermTransAlt2 data()[192] 3.472s passed
seqPermTransAlt3 data()[193] 3.476s passed
seqPermForall data()[194] 3.602s passed
seqPermExists data()[195] 3.549s passed
schiffl_lemma_2 data()[196] 23.332s passed
schiffl_thm_1 data()[197] 4.363s passed
eqSameSeq data()[198] 3.554s passed
divResZero2 data()[19] 3.565s passed
eqTermCut data()[1] 4.126s passed
divResOne1 data()[20] 3.555s passed
divResOne2 data()[21] 3.551s passed
div_cancel1 data()[22] 3.547s passed
div_cancel2 data()[23] 3.492s passed
divAddMultDenom data()[24] 3.517s passed
divMinus data()[25] 3.617s passed
divMinusDenom data()[26] 3.552s passed
divLeastDPos data()[27] 3.524s passed
divLeastDNeg data()[28] 3.509s passed
divGreatestDPos data()[29] 3.500s passed
equivAllRight data()[2] 3.978s passed
divGreatestDNeg data()[30] 3.528s passed
divIncreasingPos data()[31] 3.506s passed
divIncreasingNeg data()[32] 3.512s passed
jdiv_zero data()[33] 3.481s passed
jdivPulloutMinusNum data()[34] 3.480s passed
jdivPulloutMinusDenom data()[35] 3.552s passed
jdiv_uniquePosPos data()[36] 3.520s passed
jdiv_uniquePosNeg data()[37] 3.488s passed
jdiv_uniqueNegPos data()[38] 3.481s passed
jdiv_uniqueNegNeg data()[39] 3.494s passed
irrflConcrete1 data()[3] 3.791s passed
jdivMultDenom1 data()[40] 3.529s passed
jdivMultDenom2 data()[41] 3.498s passed
mod_geZero data()[42] 3.530s passed
mod_lessDenom data()[43] 3.492s passed
jmod_NumPos data()[44] 3.497s passed
jmod_NumNeg data()[45] 3.510s passed
jmod_geZero data()[46] 3.489s passed
jmodNumZero data()[47] 3.527s passed
jmod_pulloutminusNum data()[48] 3.506s passed
jmod_pulloutminusDenom data()[49] 3.484s passed
irrflConcrete2 data()[4] 3.760s passed
jmodUnique1 data()[50] 3.574s passed
jmodUnique2 data()[51] 3.587s passed
intDivRem data()[52] 3.474s passed
jmodjmod data()[53] 3.535s passed
jmodDivisible data()[54] 3.503s passed
jmodDivisibleRep data()[55] 3.477s passed
jdivAddMultDenom data()[56] 3.651s passed
jmodAltZero data()[57] 3.476s passed
jmodAddMultDenomZero data()[58] 3.459s passed
polyDiv_zero data()[59] 3.489s passed
cancel_gtPos data()[5] 3.678s passed
polyMod_ltdivDenom data()[60] 3.471s passed
bsum_empty data()[61] 3.470s passed
bsum_induction_upper data()[62] 3.479s passed
bsum_induction_lower data()[63] 3.501s passed
bsum_num_of_bounds data()[64] 3.476s passed
bsum_num_of_bounds2 data()[65] 3.493s passed
bsum_induction_upper2 data()[66] 3.484s passed
bsum_induction_upper_concrete data()[67] 3.468s passed
bsum_induction_upper_concrete_2 data()[68] 3.453s passed
bsum_induction_upper2_concrete data()[69] 3.482s passed
cancel_gtNeg data()[6] 3.655s passed
bsum_induction_lower_concrete data()[70] 3.504s passed
bsum_induction_lower2 data()[71] 3.488s passed
bsum_induction_lower2_concrete data()[72] 3.461s passed
bsum_positive data()[73] 3.546s passed
bsum_upper_bound data()[74] 3.519s passed
bsum_lower_bound data()[75] 3.516s passed
bsum_positive_lower_bound_element data()[76] 3.586s passed
bsum_sub_same_index data()[77] 3.561s passed
bsum_less_same_index data()[78] 3.529s passed
bsum_equal_except_one_index data()[79] 3.535s passed
moduloIntIsInInt data()[7] 3.593s passed
bsum_num_of_is_max data()[80] 3.475s passed
bsum_num_of_is_max2 data()[81] 3.524s passed
bsum_num_of_is_max3 data()[82] 3.479s passed
bsum_num_of_is_max4 data()[83] 3.485s passed
bsum_num_of_lt_max data()[84] 3.481s passed
bsum_num_of_lt_max2 data()[85] 3.489s passed
bsum_num_of_lt_max3 data()[86] 3.508s passed
bsum_num_of_lt_max4 data()[87] 3.484s passed
bsum_num_of_gt0 data()[88] 3.499s passed
bsum_num_of_gt0_alt data()[89] 3.493s passed
moduloLongIsInLong data()[8] 3.630s passed
bsum_add_concrete data()[90] 3.467s passed
bprod_all_positive data()[91] 3.510s passed
bprod_split data()[92] 3.455s passed
powConcrete0 data()[93] 3.469s passed
powConcrete1 data()[94] 3.450s passed
powSplitFactor data()[95] 3.515s passed
powAdd data()[96] 3.487s passed
powMono data()[97] 3.488s passed
powMonoConcrete data()[98] 3.443s passed
powMonoConcreteRight data()[99] 3.448s passed
moduloShortIsInShort data()[9] 3.625s passed

Standard output

396        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
424        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 12.33ms 
764        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
783        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)

1632       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1634       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1635       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1635       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3150       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9326       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.56s 
9390       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9423       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35ns 
9435       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9435       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198ns 
9438       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
12425      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
12428      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
13517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
13552      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.92ms 
13570      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
13571      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.01ms 
13573      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16583      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
16583      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
17528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
17543      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.6ms 
17547      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
17547      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.5ns 
17549      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20431      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
20432      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
21328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
21336      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ms 
21339      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
21340      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 424.9ns 
21341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24138      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
24138      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
25079      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
25096      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.97ms 
25102      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
25103      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 637.11ns 
25104      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27840      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
27840      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
28725      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
28774      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.19ms 
28779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
28779      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152ns 
28780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31497      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
31498      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
32400      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
32431      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.9ms 
32436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
32437      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 990.21ns 
32438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35143      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
35144      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
36022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
36026      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 900.31ns 
36028      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
36029      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.7ns 
36030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38778      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
38778      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
39653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
39656      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.91ns 
39663      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
39664      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 468.3ns 
39665      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42410      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
42410      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
43283      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
43285      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 798.61ns 
43287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
43287      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.9ns 
43288      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45970      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
45970      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
46843      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
46846      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.11ns 
46848      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
46848      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.8ns 
46849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49500      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
49501      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
50367      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
50370      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 749.51ns 
50372      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
50372      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.6ns 
50373      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53022      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
53023      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
53913      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
53966      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.53ms 
53976      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
53978      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.23ms 
53980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56641      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
56641      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
57478      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
57539      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.17ms 
57542      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
57542      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.2ns 
57544      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60227      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
60228      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
61092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
61251      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 149.9ms 
61254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
61254      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.69ns 
61255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63912      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
63912      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
64777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
64782      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.21ms 
64784      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
64784      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
64785      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67419      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
67420      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
68282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
68285      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
68287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
68287      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.3ns 
68288      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70924      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
70924      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
71802      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
71868      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.62ms 
71873      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
71873      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 471.11ns 
71874      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74557      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
74557      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
75394      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
75410      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.27ms 
75412      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
75412      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.6ns 
75413      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78085      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
78085      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
78959      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
78975      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.76ms 
78977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
78978      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.6ns 
78982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81635      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
81636      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
82514      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
82530      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.31ms 
82533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
82533      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 462.5ns 
82535      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85203      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
85204      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
86067      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
86081      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.38ms 
86083      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
86083      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.5ns 
86084      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88735      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
88736      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
89601      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
89628      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.62ms 
89631      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
89631      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 666.11ns 
89633      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92282      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
92282      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
93117      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
93120      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
93122      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
93122      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
93123      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95762      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
95763      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
96596      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
96637      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.76ms 
96640      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
96640      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 377.3ns 
96641      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99307      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
99307      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
100184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
100252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.26ms 
100257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
100257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.5ns 
100258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
102906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
103765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
103806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.33ms 
103808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
103808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.6ns 
103809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
106451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
107320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
107330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.83ms 
107332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
107332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.8ns 
107333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
109991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
110826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
110839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.06ms 
110841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
110841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.4ns 
110842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
113483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
114328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
114339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.26ms 
114341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
114341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.6ns 
114342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
116992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
117859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
117867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.57ms 
117869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
117869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.1ns 
117870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
120507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
121361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
121371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.79ms 
121375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
121376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 434.1ns 
121377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
124023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
124880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
124887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
124888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
124888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.9ns 
124889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
127509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
128363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
128367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
128369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
128369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.2ns 
128370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
131007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
131837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
131848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.79ms 
131849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
131849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125ns 
131850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
134493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
135351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
135399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.24ms 
135400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
135401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.9ns 
135401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
138032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
138901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
138919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.93ms 
138921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
138922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.1ns 
138924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
141530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
142383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
142407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.55ms 
142409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
142409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.4ns 
142410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
145011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
145870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
145889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.08ms 
145890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
145890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.2ns 
145891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
148536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
149366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
149382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.53ms 
149384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
149384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.6ns 
149385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
152019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
152874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
152911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.68ms 
152913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
152913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.2ns 
152914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
155540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
156405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
156409     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
156411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
156412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.7ns 
156413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
159071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
159934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
159939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
159942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
159942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.6ns 
159943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
162568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
163424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
163432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.74ms 
163434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
163434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.6ns 
163435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
166087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
166920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
166929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.12ms 
166931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
166931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.1ns 
166932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
169564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
170420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
170439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.04ms 
170441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
170441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.6ns 
170442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
173052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
173920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
173928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.16ms 
173930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
173930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.1ns 
173930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
176547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
177452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
177455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
177457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
177457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.2ns 
177458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
180095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
180956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
180961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
180966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
180967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.4ns 
180968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
183616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
184444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
184448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
184451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
184451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.2ns 
184453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
187091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
187925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
188021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 87.86ms 
188027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
188027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.2ns 
188028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
190673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
191528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
191611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.15ms 
191613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
191613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.8ns 
191614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
194232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
195083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
195086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
195088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
195088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
195089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
197733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
198584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
198620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.45ms 
198623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
198623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 405.5ns 
198624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
201267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
202094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
202124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.27ms 
202126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
202126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
202127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
204772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
205598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
205601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
205603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
205603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.2ns 
205604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
208233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
209100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
209251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 139.79ms 
209255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
209255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.7ns 
209256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
211867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
212718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
212730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.44ms 
212731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
212731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.5ns 
212732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
215331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
216179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
216188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 
216189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
216189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
216190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
218830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
219659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
219677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.87ms 
219679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
219679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.6ns 
219680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
222308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
223134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
223148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.26ms 
223150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
223150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
223151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
225765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
226614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
226618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
226620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
226620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.9ns 
226621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
229237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
230092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
230097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.05ms 
230098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
230098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
230099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
232721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
233569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
233597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.01ms 
233599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
233599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
233600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
236205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
237057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
237074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.24ms 
237076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
237076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
237077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
239724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
240550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
240567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.49ms 
240568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
240568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.1ns 
240569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
243193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
244046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
244050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
244053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
244053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.6ns 
244054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
246661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
247515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
247520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
247521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
247521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.9ns 
247522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
250114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
250967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
250972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.91ms 
250974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
250974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
250975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
253599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
254450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
254454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
254455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
254456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95ns 
254456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
257124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
257955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
257958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 791.21ns 
257960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
257960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
257960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
260593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
261442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
261446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
261448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
261448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 
261449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
264053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
264905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
264907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
264909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
264909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
264910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
267512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
268374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
268452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.03ms 
268456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
268459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.2ms 
268460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
271069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
271923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
271973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.98ms 
271976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
271976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.6ns 
271977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
274624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
275452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
275490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.09ms 
275492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
275492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.6ns 
275493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
278161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
278989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
279076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.57ms 
279077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
279078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
279078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
281744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
282602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
282638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.82ms 
282639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
282639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
282640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
285256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
286109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
286166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.11ms 
286168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
286168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
286169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
288797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
289659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
289701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.59ms 
289703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
289703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
289704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
292333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
293154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
293176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.11ms 
293178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
293178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
293179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
295813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
296672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
296699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.82ms 
296702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
296702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
296703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
299309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
300159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
300179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.91ms 
300181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
300181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.5ns 
300182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
302785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
303634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
303664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.97ms 
303665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
303665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
303666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
306266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
307119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
307145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.51ms 
307147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
307147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
307148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
309775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
310606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
310634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.2ms 
310635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
310636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108ns 
310637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
313259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
314113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
314140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.59ms 
314144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
314145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 633.71ns 
314146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
316749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
317602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
317626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.48ms 
317627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
317627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
317628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
320244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
321096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
321126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.63ms 
321127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
321127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
321128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
323732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
324592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
324619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.95ms 
324620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
324620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.8ns 
324621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
327252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
328077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
328086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms 
328087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
328087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
328088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
330719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
331575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
331595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.22ms 
331596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
331596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
331597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
334190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
335045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
335050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
335052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
335053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.4ns 
335054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
337663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
338517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
338520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 691.41ns 
338521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
338521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.6ns 
338522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
341117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
341966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
341969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 816.21ns 
341971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
341971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
341971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
344651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
345476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
345484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.13ms 
345485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
345485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
345486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
348138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
348964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
348971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.51ms 
348973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
348973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
348974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
351594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
352445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
352459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.97ms 
352461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
352461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 143.8ns 
352462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
355048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
355898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
355902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
355903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
355903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
355904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
358497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
359348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
359350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 565.5ns 
359352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
359352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
359352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
361950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
362800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
362807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
362808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
362808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
362809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
365420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
366247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
366250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.91ns 
366251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
366251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
366252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
368870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
369727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
369730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 636.71ns 
369731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
369731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
369732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
372328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
373182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
373184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 615.8ns 
373185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
373185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
373186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
375775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
376631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
376635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
376637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
376637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
376637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
379236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
380084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
380094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.64ms 
380096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
380096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
380097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
382735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
383562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
383566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
383568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
383568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
383569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
386181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
387038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
387046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.17ms 
387047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
387047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
387048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
389650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
390500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
390504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
390505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
390505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
390506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
393100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
393954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
393971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.35ms 
393972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
393972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
393973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
396578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
397431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
397438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.25ms 
397440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
397440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
397441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
400066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
400893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
400897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
400898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
400898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
400899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
403522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
404352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
404356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
404358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
404358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
404358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
406987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
407839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
407867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.36ms 
407869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
407870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.8ns 
407871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
410487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
411334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
411338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 604.81ns 
411340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
411340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
411341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
413933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
414778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
414819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.07ms 
414821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
414822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.2ns 
414823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
417469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
418305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
418309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
418311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
418311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
418312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
420948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
421776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
421800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.29ms 
421801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
421801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
421802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
424440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
425294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
425315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.65ms 
425317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
425317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
425318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
427945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
428801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
428826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.92ms 
428827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
428828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116ns 
428828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
431419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
432274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
432277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 690.01ns 
432280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
432280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
432280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
434899     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
435723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
435736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.41ms 
435739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
435739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.6ns 
435740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
438353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
439219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
439222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
439223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
439224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
439224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
441809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
442672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
442675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 803.91ns 
442676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
442676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
442677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
445284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
446113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
446115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 966.81ns 
446117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
446117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
446118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
448733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
449592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
449596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
449597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
449597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
449598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
452209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
453062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
453065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
453067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
453067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
453067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
455656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
456511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
456521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.12ms 
456522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
456522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
456523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
459137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
459989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
460001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.89ms 
460003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
460003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
460004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
462604     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
463461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
463472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ms 
463475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
463475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.1ns 
463476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
466070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
466929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
466941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.61ms 
466944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
466944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210ns 
466945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
469577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
470443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
470449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.78ms 
470451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
470451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
470451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
473046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
473906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
473912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
473914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
473914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
473914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
476527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
477365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
477368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 706.31ns 
477369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
477369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
477370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
480011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
480882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
480885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
480886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
480886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
480887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
483497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
484363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
484366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 869.81ns 
484367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
484367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
484368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
487019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
487888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
487900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ms 
487902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
487902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
487903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
490533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
491402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
491406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
491408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
491408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
491409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
494035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
494871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
494878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
494880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
494880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
494881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
497527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
498397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
498400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 851.71ns 
498401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
498401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
498402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
501014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
501897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
501899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 678.01ns 
501901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
501901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
501901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
504518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
505377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
505381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
505383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
505383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
505384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
507964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
508827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
508831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
508832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
508832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
508833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
511438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
512301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
512305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
512306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
512306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
512307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
514903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
515764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
515767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
515768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
515768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
515769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
518374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
519240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
519246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
519247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
519247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
519248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
521867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
522734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
522737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
522739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
522739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
522740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
525375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
526240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
526251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.93ms 
526253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
526253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
526253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
528859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
529721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
529724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 699.91ns 
529725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
529725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
529726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
532339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
533200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
533207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.24ms 
533209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
533209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
533209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
535800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
536659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
536662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 975.51ns 
536664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
536664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
536664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
539293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
540157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
540159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 876.61ns 
540161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
540161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
540162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
542783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
543622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
543628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
543629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
543630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
543630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
546242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
547102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
547106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
547107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
547107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
547108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
549732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
550600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
550603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
550605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
550605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
550606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
553210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
554072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
554076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
554078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
554078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
554078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
556703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
557572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
557577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.37ms 
557579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
557579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
557580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
560209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
561070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
561084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.55ms 
561086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
561086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
561087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
563669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
564526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
564541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ms 
564543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
564543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
564544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
567153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
568018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
568028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.74ms 
568030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
568030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
568031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
570644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
571501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
571512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.91ms 
571513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
571513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
571514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
574090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
574949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
574975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.3ms 
574976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
574976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
574977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
577577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
578439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
578463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.51ms 
578465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
578465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
578466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
581086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
581948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
581972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.3ms 
581974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
581974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
581974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
584581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
585420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
585434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.26ms 
585436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
585436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
585437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
588040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
588902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
588933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.12ms 
588934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
588934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
588935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
591546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
592410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
592457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.59ms 
592458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
592458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
592459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
595064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
595928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
595966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.24ms 
595968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
595968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
595969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
598589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
599429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
599505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.3ms 
599507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
599507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.6ns 
599507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
602103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
602970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
603013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.28ms 
603015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
603015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
603016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
605630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
606493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
606613     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 114.34ms 
606615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
606615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
606616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
609230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
610095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
610103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.98ms 
610104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
610104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
610105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
612732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
613598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
613606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.92ms 
613608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
613608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
613608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
616258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
617122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
617127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
617128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
617129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
617129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
619741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
619741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
620610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
620629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.27ms 
620630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
620631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
620631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
623224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
624085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
624096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.86ms 
624099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
624099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.1ns 
624099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
626712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
627575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
627579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
627580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
627580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
627581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
630208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
631069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
631086     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.76ms 
631088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
631088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
631089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
633699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
634563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
634581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.24ms 
634584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
634584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
634584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
637229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
638129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
638149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.36ms 
638151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
638151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
638151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
640786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
641653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
641657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
641658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
641658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
641659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
644278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
645142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
645146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.86ms 
645148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
645148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.32ns 
645149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
647770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
648632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
648639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 
648640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
648640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
648641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
651264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
652131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
652138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
652139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
652139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
652140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
654733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
655593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
655664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.9ms 
655666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
655666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
655667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
658295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
659169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
659198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.51ms 
659199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
659199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
659200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
661812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
662676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
662699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.77ms 
662701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
662701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
662702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
665308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
666172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
666174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 321ns 
666176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
666176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
666177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
668784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
669646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
669844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 187.55ms 
669846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
669846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
669847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
672464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
673335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
673387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.61ms 
673389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
673389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
673389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
676038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
676899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
676902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 395.41ns 
676904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
676906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.55ms 
676907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
679503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
680367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
680369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 400.71ns 
680370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
680370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
680371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
682977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
683839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
683841     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 437.31ns 
683843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
683843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
683844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
686454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
687315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
687317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 542.31ns 
687318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
687319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
687319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
689943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
689943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
690803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
690899     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
690918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.44ms 
690922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
690922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285ns 
690925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
693557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
694419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
694467     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
694468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.84ms 
694470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
694470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.4ns 
694475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
697098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
697961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
697963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ns 
697994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
698047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
698065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
698070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
698076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
698079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
698080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
698082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
698085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
698087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
698090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
698091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
698313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
698315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
698316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
698319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
698320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
698453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
698455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
698458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
698460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
698461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
698462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
698631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
698634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
698635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
698636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
698638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
698641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
698798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
698800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
698801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
698801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
698802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
698803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
698812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
698813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
698814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
698816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
698819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
698820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
698831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
698832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
698833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
698834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
698836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
698836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
699001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
699002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
699004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
699140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
699142     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)'' 
699145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
699146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
699148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
699149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
699150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
699150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
699154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
699156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
699157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
699158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
699159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
699272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
699276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
699278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
699279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
699280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
699281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
699282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
699401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
699403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
699404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
699406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
699407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
699408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
699409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
699410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
699502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
699504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
699637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
699645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
699653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
699655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
699657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
699659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
699660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
699661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
699662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
699664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
699676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
699684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
699818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
699820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
699821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
699822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
699823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
699824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
699824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
699825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
699880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
699886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
699983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
699985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
699987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
699988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
699989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
699990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
700165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
700173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
700176     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)'' 
700178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
700179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
700183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
700183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
700184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
700193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
700198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
700200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
700200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
700295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
700296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
700297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
700298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
700299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
700300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
700415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
700417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
700418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
700420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
700421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
700422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
700422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
700423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
700502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
700504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
700580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
700581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
700582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
700586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
700590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
700596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
700724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
700725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
700726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
700728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
700740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
700828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
704524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
704526     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)'' 
704533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
704539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
704539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
704540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
704541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
704550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
704551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
704552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
704553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
704554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
704651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
704655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
704657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
704658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
704658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
704659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
704660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
704756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
704758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
704759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
704760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
704761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
704762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
704762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
704763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
704841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
704842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
704918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
704922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
704927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
704928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
704929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
704930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
704940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
705023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
705024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
705025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
705026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
705103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
705113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
705115     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)'' 
705117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
705118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
705119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
705119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
705120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
705131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
705133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
705134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
705135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
705136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
705226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
705228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
705230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
705231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
705232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
705325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
705333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
705335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
705335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
705336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
705336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
705337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
705440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
705441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
705442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
705444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
705444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
705446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
705447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
705448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
705449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
705449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
705450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
705451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
705451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
705452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
705452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
705547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
705549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
705555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
705638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
705725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
705727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
705728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
705729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
705730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
705731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
705731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
705732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
705733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
705824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
705831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
705931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
705932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
705933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
705935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
705936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
705936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
705937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
705938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
705944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
705945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
706029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
706037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
706044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
706153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
706154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
706155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
706156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
706156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
706157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
706157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
706158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
706214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
706219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
706220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
706221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
706222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
706228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
706235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
706399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
706489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
706490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
706491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
706492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
706665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
706756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
706757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
709895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
709900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
709902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
709903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
709904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
710018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
710019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
710020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
710021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
710021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
710127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
713216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
716486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
716490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
716492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
716492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
716493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
716608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
716610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
716611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
716612     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)' ...' 
716613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
717802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
717802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.5ns 
717803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
720480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
721368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
721369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
721370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
721378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
721390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
721393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
721395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
721395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
721400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
721401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
721405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
721407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
721408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
721418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
721419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
721420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
721465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
721467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
721467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
721468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
721468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
721602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
721603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
721604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
721605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
721606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
721610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
721610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
721611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
721612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
721613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
721614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
721694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
721695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
721696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
721697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
721698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
721698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
721784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
721785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
721786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
721786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
721787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
721788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
721788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
721789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
721790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
721790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
721791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
721791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
721792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
721792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
721793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
721794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
721794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
721795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
721796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
721798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
721837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
721839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
721901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
721902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
721904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
721905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
721906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
721906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
721962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
721965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
721966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
721968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
721969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
721970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
721970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
722028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
722031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
722035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
722101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
722166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
722167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.1ns 
722168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
724774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
725676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
725718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.71ms

Standard error

ANTLR Tool version 4.12.0 used for code generation does not match the current runtime version 4.13.0
ANTLR Tool version 4.12.0 used for code generation does not match the current runtime version 4.13.0
ANTLR Tool version 4.12.0 used for code generation does not match the current runtime version 4.13.0
ANTLR Tool version 4.12.0 used for code generation does not match the current runtime version 4.13.0