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

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

tests
0

failures
0

ignored
9m57.33s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 2.869s passed
powPositiveConcrete data()[101] 2.879s passed
powGeq1Concrete data()[102] 2.867s passed
pow2InIntLower data()[103] 2.866s passed
pow2InIntUpper data()[104] 2.875s passed
logSelfConcrete data()[105] 2.869s passed
log1Concrete data()[106] 2.877s passed
logProduct data()[107] 2.886s passed
logTimesBaseConcrete data()[108] 2.876s passed
logProdIdentity data()[109] 2.871s passed
moduloByteIsInByte data()[10] 2.955s passed
logProdIdentityConcrete data()[110] 2.883s passed
logPowIdentity data()[111] 2.856s passed
logPowIdentityConcrete data()[112] 2.877s passed
logPositive data()[113] 2.871s passed
logPositiveConcrete data()[114] 2.876s passed
logMono data()[115] 2.885s passed
logMonoConcrete data()[116] 2.877s passed
powLogLess data()[117] 2.901s passed
powLogMore2 data()[118] 2.884s passed
logLessThanPow data()[119] 2.923s passed
moduloCharIsInChar data()[11] 2.923s passed
logLessThanPowConcrete data()[120] 2.859s passed
logSqueeze data()[121] 2.881s passed
ifthenelse_equals data()[122] 2.885s passed
ifthenelse_equals_1 data()[123] 2.866s passed
ifthenelse_equals_2 data()[124] 2.882s passed
disjointWithSingleton1 data()[125] 2.886s passed
disjointWithSingleton2 data()[126] 2.867s passed
disjointArrayRanges data()[127] 2.892s passed
disjointArrayRangeAllFields1 data()[128] 2.897s passed
disjointArrayRangeAllFields2 data()[129] 2.892s passed
div_unique1 data()[12] 3.075s passed
seqSelfDefinition data()[130] 2.918s passed
seqOutsideValue data()[131] 2.910s passed
castedGetAny data()[132] 2.899s passed
seqGetAlphaCast data()[133] 2.896s passed
getOfSeqSingleton data()[134] 2.893s passed
getOfSeqSingletonConcrete data()[135] 2.892s passed
getOfSeqConcat data()[136] 2.898s passed
getOfSeqSub data()[137] 2.910s passed
getOfSeqReverse data()[138] 2.895s passed
lenOfSeqEmpty data()[139] 2.895s passed
div_unique2 data()[13] 3.048s passed
lenOfSeqSingleton data()[140] 2.876s passed
lenOfSeqConcat data()[141] 2.892s passed
lenOfSeqSub data()[142] 2.894s passed
lenOfSeqReverse data()[143] 2.894s passed
equalityToSeqGetAndSeqLenLeft data()[144] 2.927s passed
equalityToSeqGetAndSeqLenRight data()[145] 2.891s passed
getOfSeqSingletonEQ data()[146] 2.888s passed
getOfSeqConcatEQ data()[147] 2.902s passed
getOfSeqSubEQ data()[148] 2.890s passed
getOfSeqReverseEQ data()[149] 2.899s passed
div_exists data()[14] 3.146s passed
lenOfSeqEmptyEQ data()[150] 2.893s passed
lenOfSeqSingletonEQ data()[151] 2.884s passed
lenOfSeqConcatEQ data()[152] 2.890s passed
lenOfSeqSubEQ data()[153] 2.884s passed
lenOfSeqReverseEQ data()[154] 2.889s passed
getOfSeqDefEQ data()[155] 2.894s passed
lenOfSeqDefEQ data()[156] 2.886s passed
seqConcatWithSeqEmpty1 data()[157] 2.897s passed
seqConcatWithSeqEmpty2 data()[158] 2.899s passed
seqReverseOfSeqEmpty data()[159] 2.893s passed
div_one data()[15] 2.979s passed
subSeqComplete data()[160] 2.919s passed
subSeqTailR data()[161] 2.911s passed
subSeqTailL data()[162] 2.907s passed
subSeqTailEQR data()[163] 2.912s passed
subSeqTailEQL data()[164] 2.897s passed
seqDef_split data()[165] 2.941s passed
seqDef_induction_upper data()[166] 2.930s passed
seqDef_induction_upper_concrete data()[167] 2.924s passed
seqDef_induction_lower data()[168] 2.943s passed
seqDef_induction_lower_concrete data()[169] 2.927s passed
jdiv_one data()[16] 2.908s passed
seqDef_split_in_three data()[170] 3.005s passed
seqDef_empty data()[171] 2.933s passed
seqDef_one_summand data()[172] 2.888s passed
seqDef_lower_equals_upper data()[173] 2.883s passed
seqDefOfSeq data()[174] 2.918s passed
seqSelfDefinitionEQ2 data()[175] 2.901s passed
indexOfSeqSingleton data()[176] 2.903s passed
indexOfSeqConcatFirst data()[177] 2.899s passed
indexOfSeqConcatSecond data()[178] 2.904s passed
indexOfSeqSub data()[179] 2.914s passed
div_zero data()[17] 2.956s passed
lenOfArray2seq data()[180] 2.885s passed
getAnyOfArray2seq data()[181] 2.903s passed
getOfArray2seq data()[182] 2.880s passed
getAnyOfNPermInv data()[183] 2.897s passed
seqNPermRange data()[184] 2.945s passed
seqPermTrans data()[185] 2.923s passed
seqPermRefl data()[186] 2.912s passed
seqPermSplit data()[187] 2.877s passed
seqNPermRight data()[188] 3.096s passed
seqPermFromSwap data()[189] 2.959s passed
divResZero1 data()[18] 2.939s passed
seqPermTransAlt0 data()[190] 2.885s passed
seqPermTransAlt1 data()[191] 2.909s passed
seqPermTransAlt2 data()[192] 2.899s passed
seqPermTransAlt3 data()[193] 2.874s passed
seqPermForall data()[194] 2.976s passed
seqPermExists data()[195] 3.037s passed
schiffl_lemma_2 data()[196] 21.521s passed
schiffl_thm_1 data()[197] 3.679s passed
eqSameSeq data()[198] 3.006s passed
divResZero2 data()[19] 2.967s passed
eqTermCut data()[1] 3.475s passed
divResOne1 data()[20] 2.954s passed
divResOne2 data()[21] 3.020s passed
div_cancel1 data()[22] 3.028s passed
div_cancel2 data()[23] 3.029s passed
divAddMultDenom data()[24] 3.031s passed
divMinus data()[25] 2.992s passed
divMinusDenom data()[26] 2.947s passed
divLeastDPos data()[27] 2.909s passed
divLeastDNeg data()[28] 2.915s passed
divGreatestDPos data()[29] 2.920s passed
equivAllRight data()[2] 3.205s passed
divGreatestDNeg data()[30] 2.913s passed
divIncreasingPos data()[31] 2.902s passed
divIncreasingNeg data()[32] 2.890s passed
jdiv_zero data()[33] 2.912s passed
jdivPulloutMinusNum data()[34] 2.920s passed
jdivPulloutMinusDenom data()[35] 2.943s passed
jdiv_uniquePosPos data()[36] 2.905s passed
jdiv_uniquePosNeg data()[37] 2.907s passed
jdiv_uniqueNegPos data()[38] 2.900s passed
jdiv_uniqueNegNeg data()[39] 2.887s passed
irrflConcrete1 data()[3] 3.226s passed
jdivMultDenom1 data()[40] 2.920s passed
jdivMultDenom2 data()[41] 2.873s passed
mod_geZero data()[42] 2.899s passed
mod_lessDenom data()[43] 2.890s passed
jmod_NumPos data()[44] 2.905s passed
jmod_NumNeg data()[45] 2.895s passed
jmod_geZero data()[46] 2.873s passed
jmodNumZero data()[47] 2.948s passed
jmod_pulloutminusNum data()[48] 2.869s passed
jmod_pulloutminusDenom data()[49] 2.879s passed
irrflConcrete2 data()[4] 3.068s passed
jmodUnique1 data()[50] 2.950s passed
jmodUnique2 data()[51] 2.956s passed
intDivRem data()[52] 2.889s passed
jmodjmod data()[53] 2.933s passed
jmodDivisible data()[54] 2.896s passed
jmodDivisibleRep data()[55] 2.869s passed
jdivAddMultDenom data()[56] 3.022s passed
jmodAltZero data()[57] 2.886s passed
jmodAddMultDenomZero data()[58] 2.902s passed
polyDiv_zero data()[59] 2.878s passed
cancel_gtPos data()[5] 3.130s passed
polyMod_ltdivDenom data()[60] 2.893s passed
bsum_empty data()[61] 2.867s passed
bsum_induction_upper data()[62] 2.892s passed
bsum_induction_lower data()[63] 2.887s passed
bsum_num_of_bounds data()[64] 2.895s passed
bsum_num_of_bounds2 data()[65] 2.893s passed
bsum_induction_upper2 data()[66] 2.866s passed
bsum_induction_upper_concrete data()[67] 2.884s passed
bsum_induction_upper_concrete_2 data()[68] 2.868s passed
bsum_induction_upper2_concrete data()[69] 2.881s passed
cancel_gtNeg data()[6] 3.153s passed
bsum_induction_lower_concrete data()[70] 2.869s passed
bsum_induction_lower2 data()[71] 2.860s passed
bsum_induction_lower2_concrete data()[72] 2.898s passed
bsum_positive data()[73] 2.905s passed
bsum_upper_bound data()[74] 2.937s passed
bsum_lower_bound data()[75] 2.900s passed
bsum_positive_lower_bound_element data()[76] 2.926s passed
bsum_sub_same_index data()[77] 2.901s passed
bsum_less_same_index data()[78] 2.941s passed
bsum_equal_except_one_index data()[79] 2.908s passed
moduloIntIsInInt data()[7] 3.047s passed
bsum_num_of_is_max data()[80] 2.885s passed
bsum_num_of_is_max2 data()[81] 2.912s passed
bsum_num_of_is_max3 data()[82] 2.880s passed
bsum_num_of_is_max4 data()[83] 2.905s passed
bsum_num_of_lt_max data()[84] 2.893s passed
bsum_num_of_lt_max2 data()[85] 2.899s passed
bsum_num_of_lt_max3 data()[86] 2.892s passed
bsum_num_of_lt_max4 data()[87] 2.875s passed
bsum_num_of_gt0 data()[88] 2.898s passed
bsum_num_of_gt0_alt data()[89] 2.880s passed
moduloLongIsInLong data()[8] 2.988s passed
bsum_add_concrete data()[90] 2.884s passed
bprod_all_positive data()[91] 2.877s passed
bprod_split data()[92] 2.877s passed
powConcrete0 data()[93] 2.865s passed
powConcrete1 data()[94] 2.882s passed
powSplitFactor data()[95] 2.869s passed
powAdd data()[96] 2.870s passed
powMono data()[97] 2.897s passed
powMonoConcrete data()[98] 2.859s passed
powMonoConcreteRight data()[99] 2.885s passed
moduloShortIsInShort data()[9] 2.966s passed

Standard output

636        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
659        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.75ms 
858        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
880        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)

1820       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1822       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1825       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1825       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3058       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7822       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.96s 
7885       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7917       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33ns 
7928       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7929       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.5ns 
7933       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10530      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
10532      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11374      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11396      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.33ms 
11417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11417      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.1ns 
11418      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13794      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
13794      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
14597      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
14615      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.23ms 
14619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
14619      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.5ns 
14624      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17046      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
17046      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
17837      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
17843      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
17845      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
17845      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.3ns 
17847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20108      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
20109      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
20892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
20910      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.57ms 
20917      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
20917      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258ns 
20921      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23199      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
23200      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24004      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24044      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.49ms 
24048      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24049      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.8ns 
24051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26395      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
26396      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
27180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
27199      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.65ms 
27202      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
27203      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.9ns 
27204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29463      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
29463      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
30244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
30247      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 769.7ns 
30250      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
30250      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.7ns 
30251      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32484      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
32484      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
33234      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
33237      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 530.2ns 
33238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
33243      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.7ms 
33244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35476      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
35477      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
36199      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
36202      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 515.6ns 
36205      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
36206      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.5ns 
36207      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38423      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
38423      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
39155      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
39158      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 560.6ns 
39160      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
39160      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.7ns 
39162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41351      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
41351      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
42079      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
42081      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 484ns 
42083      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
42084      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.5ns 
42085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44343      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
44344      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
45069      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
45156      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.88ms 
45158      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
45158      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.3ns 
45159      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47395      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
47395      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
48134      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
48203      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.82ms 
48210      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
48211      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 569.3ns 
48212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50413      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
50413      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
51131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
51354      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 213.93ms 
51357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
51357      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.2ns 
51358      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53556      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
53557      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
54329      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
54334      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
54336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
54337      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.4ns 
54338      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56536      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
56537      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
57239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
57242      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
57245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
57245      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.6ns 
57246      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59439      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
59440      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
60162      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
60200      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.15ms 
60202      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
60202      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 330.8ns 
60203      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62423      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
62423      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
63123      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
63139      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.57ms 
63141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
63141      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288ns 
63142      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65372      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.23s 
65373      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
66091      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
66106      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.82ms 
66109      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
66111      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.77ms 
66115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
68313      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
69046      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
69061      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ms 
69063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
69063      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.6ns 
69064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71322      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
71322      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
72067      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
72081      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.35ms 
72083      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
72083      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.7ns 
72084      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74343      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
74344      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
75086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
75109      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.72ms 
75110      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
75111      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.9ns 
75111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77388      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
77388      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
78136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
78139      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
78140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
78140      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
78141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80386      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
80386      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
81130      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
81169      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.22ms 
81171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
81171      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.8ns 
81172      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83413      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.24s 
83414      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
84109      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
84162      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.29ms 
84164      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
84165      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 830.39ns 
84166      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86357      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
86358      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
87071      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
87109      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.4ms 
87111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
87111      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
87112      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89295      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
89296      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
90012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
90019      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
90020      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
90020      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
90021      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92204      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
92205      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
92920      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
92933      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.29ms 
92934      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
92934      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
92935      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95123      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
95123      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
95844      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
95854      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.72ms 
95855      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
95855      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
95856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98041      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
98041      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
98760      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
98767      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.61ms 
98770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
98770      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
98770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
100942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
101664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
101670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
101672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
101673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.7ns 
101674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
103857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
104555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
104561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.32ms 
104562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
104562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
104563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
106749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
107468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
107473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
107478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
107478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.3ns 
107479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
109673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
110386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
110396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.89ms 
110398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
110398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.8ns 
110399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
112579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
113295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
113339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.43ms 
113341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
113342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.3ns 
113343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
115504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
116222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
116245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.76ms 
116247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
116247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
116248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
118428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
119137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
119152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.55ms 
119154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
119154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168ns 
119155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
121323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
122037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
122052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.53ms 
122053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
122053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
122054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
124233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
124924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
124940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.72ms 
124941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
124941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
124941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
127115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
127825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
127859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.53ms 
127861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
127861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
127861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
130037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
130730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
130733     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
130734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
130734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
130734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
132916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
133628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
133632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
133633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
133633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
133634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
135799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
136512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
136520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.05ms 
136524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
136524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
136526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
138703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
139414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
139427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.39ms 
139429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
139429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
139430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
141596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
142307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
142323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.85ms 
142325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
142325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
142325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
144499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
145189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
145196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
145198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
145198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
145198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
147387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
148143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
148145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
148150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
148151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.28ms 
148152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
150325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
151014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
151018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
151019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
151019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
151020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
153185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
153894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
153897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
153898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
153898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
153899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
156057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
156775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
156846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.15ms 
156848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
156848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 447.6ns 
156849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
159025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
159733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
159802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.24ms 
159804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
159804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.8ns 
159805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
161977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
162687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
162690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
162693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
162693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.3ns 
162694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
164885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
165591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
165624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.1ms 
165625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
165625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.7ns 
165626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
167785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
168496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
168521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.84ms 
168522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
168522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
168523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
170699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
171388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
171390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 964.79ns 
171391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
171391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
171392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
173565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
174273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
174411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 128.54ms 
174412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
174412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
174413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
176598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
177287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
177297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ms 
177298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
177300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.11ms 
177302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
179483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
180192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
180199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.09ms 
180200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
180200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
180201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
182352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
183063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
183078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.88ms 
183079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
183079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
183079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
185249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
185959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
185970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.05ms 
185971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
185972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
185972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
188125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
188834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
188838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
188840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
188840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
188840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
191007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
191697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
191729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
191732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
191732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
191733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
193888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
194597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
194617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.86ms 
194619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
194619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
194619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
196809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
197498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
197512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.67ms 
197513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
197513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
197514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
199685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
200392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
200406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.09ms 
200407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
200407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
200407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
202558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
203268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
203272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
203274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
203274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.4ns 
203275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
205446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
206152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
206156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
206157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
206157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
206158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
208311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
209019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
209024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.08ms 
209025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
209025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.1ns 
209026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
211194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
211903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
211906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
211907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
211907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
211908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
214065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
214773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
214775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.6ns 
214776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
214776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
214777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
216945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
217632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
217636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
217637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
217637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
217638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
219822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
220532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
220534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 812.7ns 
220535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
220535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
220536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
222687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
223394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
223439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.69ms 
223441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
223441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
223441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
225621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
226328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
226375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.64ms 
226377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
226377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.7ns 
226378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
228537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
229244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
229276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.15ms 
229277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
229277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
229278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
231448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
232155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
232203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44ms 
232204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
232204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
232205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
234360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
235074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
235104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.21ms 
235105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
235106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
235106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
237276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
237965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
238045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.82ms 
238046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
238046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
238047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
240203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
240910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
240938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.93ms 
240955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
240955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
240955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
243132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
243820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
243839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.16ms 
243840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
243840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
243841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
246021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
246729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
246751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.84ms 
246752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
246752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
246753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
248906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
249613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
249631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.08ms 
249632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
249632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
249633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
251799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
252511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
252536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.17ms 
252538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
252538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 182.4ns 
252539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
254698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
255406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
255429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.16ms 
255430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
255430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
255431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
257599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
258306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
258329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.47ms 
258330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
258330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
258331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
260489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
261199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
261221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.48ms 
261222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
261222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
261223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
263389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
264077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
264096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.69ms 
264097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
264097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
264098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
266266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
266971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
266994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.3ms 
266995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
266995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
266996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
269163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
269852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
269875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.51ms 
269876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
269876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
269877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
272041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
272748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
272758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.78ms 
272760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
272760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.4ns 
272761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
274912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
275621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
275636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.21ms 
275637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
275637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
275638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
277803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
278511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
278514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
278515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
278515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
278516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
280668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
281377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
281379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 540ns 
281380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
281380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
281381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
283548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
284258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
284260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 693.5ns 
284261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
284261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
284262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
286414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
287123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
287129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
287131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
287131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.7ns 
287132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
289304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
289995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
290000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
290002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
290002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.8ns 
290003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
292175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
292887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
292898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.74ms 
292899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
292899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
292899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
295045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
295754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
295757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
295758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
295758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
295758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
297932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
298641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
298642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 565.5ns 
298644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
298644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
298644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
300798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
301506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
301511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
301512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
301512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
301513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
303682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
304388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
304390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 488.7ns 
304391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
304391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.2ns 
304392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
306546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
307254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
307256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 504.8ns 
307257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
307258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
307258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
309432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
310121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
310123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 541.5ns 
310124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
310124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
310124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
312287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
312995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
312998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
312999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
312999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.1ns 
312999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
315149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
315859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
315867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.06ms 
315868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
315868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
315869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
318033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
318740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
318744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
318745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
318745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.3ns 
318745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
320913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
321624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
321630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.51ms 
321631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
321631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45ns 
321632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
323796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
324502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
324505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
324506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
324506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
324507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
326655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
327363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
327377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.68ms 
327378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
327378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
327379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
329550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
330257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
330260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
330261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
330261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
330261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.14s 
332406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
333114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
333117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
333118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
333118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.5ns 
333118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
335282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
335990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
335994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
335995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
335995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 42.3ns 
335996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.15s 
338141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
338849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
338865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.11ms 
338866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
338866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
338867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
341030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
341736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
341740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 460.1ns 
341741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
341741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
341742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
343901     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
344591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
344626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.06ms 
344627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
344627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
344627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
346791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
347498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
347502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
347503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
347503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.4ns 
347504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
349671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
350380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
350404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.72ms 
350406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
350406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.3ns 
350407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
352563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
353270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
353289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.26ms 
353290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
353290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
353291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
355482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
356189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
356212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.2ms 
356213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
356213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
356214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
358379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
359068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
359070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 582.2ns 
359071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
359071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44ns 
359072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
361235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
361947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
361952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
361953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
361953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.9ns 
361954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
364122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
364834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
364836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
364838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
364838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.4ns 
364839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
367004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
367701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
367703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 640.9ns 
367704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
367704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
367705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
369870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
370582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
370584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 755.89ns 
370587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
370587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.5ns 
370588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
372755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
373469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
373472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
373476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
373477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.4ns 
373477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
375644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
376338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
376341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
376342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
376342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
376343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
378511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
379225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
379234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.58ms 
379235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
379235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
379236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
381405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
382118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
382131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.21ms 
382133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
382133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 170.3ns 
382134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
384301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
385012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
385024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.72ms 
385025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
385025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
385025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
387183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
387903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
387941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.23ms 
387943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
387943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.3ns 
387944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
390127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
390848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
390852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
390853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
390853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
390854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
393028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
393745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
393750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ms 
393751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
393751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.1ns 
393752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
395924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
396643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
396646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 725.2ns 
396648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
396648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.4ns 
396649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
398833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
399536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
399539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
399541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
399541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
399541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
401712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
402430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
402432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 912.99ns 
402433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
402433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
402434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
404602     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
405319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
405329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.08ms 
405331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
405331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.2ns 
405332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
407518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
408236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
408240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
408241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
408241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
408241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
410411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
411128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
411135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
411136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
411136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.9ns 
411137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
413311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
414028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
414030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.89ns 
414032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
414032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
414033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
416205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
416904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
416906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 555.7ns 
416907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
416907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
416907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
419075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
419794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
419798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
419799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
419799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
419800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
421969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
422689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
422692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
422693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
422693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
422694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
424865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
425583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
425586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
425587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
425587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.4ns 
425588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.2s 
427792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
428510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
428513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
428514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
428514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
428515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
430682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
431399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
431404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.41ms 
431405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
431405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
431406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
433571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
434289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
434291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
434293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
434293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
434293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
436466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
437184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
437194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.96ms 
437196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
437196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.9ns 
437197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
439366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
440082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
440084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 784.39ns 
440085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
440085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
440086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
442259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
442978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
442984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
442985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
442985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
442986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
445159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
445875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
445877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822.89ns 
445878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
445878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.2ns 
445879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
448044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
448760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
448762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 841.09ns 
448763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
448763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
448764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
450931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
451648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
451652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.91ms 
451653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
451653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.4ns 
451654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
453817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
454534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
454537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
454538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
454538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
454538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
456705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
457423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
457426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
457427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
457427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
457427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
459599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
460317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
460320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
460322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
460322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
460323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
462484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
463203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
463207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
463208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
463209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
463209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
465372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
466092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
466105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.57ms 
466106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
466106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
466107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
468273     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
468990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
469004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ms 
469005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
469005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
469006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
471190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
471888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
471898     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.92ms 
471899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
471899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
471900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474087     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
474087     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
474806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
474816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.31ms 
474817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
474817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
474818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
476985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
477704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
477728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.92ms 
477729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
477729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
477730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
479896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
480612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
480636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.46ms 
480637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
480637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
480638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
482806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
483526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
483548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.17ms 
483549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
483549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
483550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
485714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
486431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
486445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.37ms 
486446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
486446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
486446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
488640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
489358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
489386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.74ms 
489387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
489387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
489388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
491552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
492272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
492315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.24ms 
492316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
492316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
492317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
494485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
495204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
495239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.31ms 
495240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
495241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
495241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
497427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
498144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
498182     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.75ms 
498184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
498184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
498184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
500353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
501070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
501110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.78ms 
501112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
501112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
501112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
503277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
503999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
504115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 106.9ms 
504117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
504117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.7ns 
504118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
506323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
507041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
507048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.55ms 
507049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
507049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
507050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
509213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
509930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
509936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
509939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
509939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.5ns 
509940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
512100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
512816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
512821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
512822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
512822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
512822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
515006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
515723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
515739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.82ms 
515740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
515740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
515741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
517911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
518631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
518641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.19ms 
518642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
518642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
518643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
520807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
521540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
521543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
521544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
521544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
521545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
523711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
524427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
524443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.83ms 
524444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
524444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
524445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
526615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
527333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
527348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.96ms 
527349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
527349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
527349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
529529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
530245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
530263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.22ms 
530264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
530264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
530264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
532428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
533145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
533147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
533149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
533149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
533150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
535330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
536047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
536051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
536052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
536052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
536052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
538210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
538925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
538930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
538931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
538931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
538932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
541107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
541822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
541828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
541829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
541829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.4ns 
541829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
543990     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
544707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
544772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.76ms 
544773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
544773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
544774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
546953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
547671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
547696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.68ms 
547697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
547697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
547697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
549872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
550587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
550607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.28ms 
550608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
550608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
550609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
552766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
553483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
553485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 232.1ns 
553486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
553486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.9ns 
553487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
555679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
556396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
556580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 174.63ms 
556582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
556582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.3ns 
556583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.19s 
558770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
559489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
559540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.4ms 
559542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
559542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
559542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
561706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
562424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
562426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 263.3ns 
562426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
562427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46ns 
562427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
564608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
565328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
565335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 294.1ns 
565336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
565337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.6ns 
565337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.18s 
567514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
568232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
568234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 291.9ns 
568235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
568235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.6ns 
568235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.16s 
570392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
571107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
571108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 411.2ns 
571109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
571110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
571110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
573280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
574000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
574066     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
574083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.9ms 
574086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
574086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.5ns 
574087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.26s 
576347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
577074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
577119     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
577120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.43ms 
577122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
577122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.1ns 
577123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.17s 
579298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
580019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
580020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ns 
580043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
580110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
580134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
580141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
580148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
580151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
580152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
580155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
580159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
580161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
580165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
580168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
580360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
580361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
580362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
580363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
580364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
580480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
580481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
580482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
580483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
580484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
580485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
580660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
580661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
580662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
580662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
580663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
580664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
580787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
580788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
580789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
580789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
580790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
580791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
580797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
580798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
580798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
580800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
580801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
580801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
580808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
580808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
580809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
580810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
580810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
580811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
580971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
580974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
580975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
581088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
581089     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)'' 
581091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
581092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
581093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
581094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
581095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
581097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
581100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
581101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
581102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
581103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
581104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
581205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
581209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
581210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
581210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
581211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
581212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
581214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
581332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
581336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
581337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
581338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
581339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
581339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
581340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
581342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
581452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
581453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
581565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
581569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
581574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
581575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
581577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
581579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
581579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
581580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
581580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
581581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
581590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
581594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
581713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
581715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
581716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
581718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
581718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
581719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
581719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
581720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
581774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
581779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
581871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
581872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
581874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
581876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
581876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
581878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
582033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
582037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
582040     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)'' 
582041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
582043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
582043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
582044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
582045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
582054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
582059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
582061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
582061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
582167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
582168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
582168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
582169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
582170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
582171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
582275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
582277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
582278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
582279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
582280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
582280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
582281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
582283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
582372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
582373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
582455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
582456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
582457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
582461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
582465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
582470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
582598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
582599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
582600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
582601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
582611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
582694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
586162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
586163     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)'' 
586168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
586169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
586169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
586170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
586170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
586177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
586179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
586180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
586180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
586181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
586269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
586273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
586274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
586274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
586275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
586275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
586276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
586368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
586369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
586370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
586375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
586375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
586376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
586376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
586377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
586449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
586450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
586523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
586527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
586531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
586532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
586533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
586533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
586543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
586623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
586624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
586624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
586625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
586693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
586702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
586702     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)'' 
586704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
586705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
586705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
586706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
586706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
586716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
586717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
586718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
586718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
586719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
586801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
586803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
586804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
586804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
586805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
586891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
586895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
586896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
586896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
586897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
586897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
586898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
587029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
587030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
587031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
587032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
587032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
587033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
587033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
587034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
587034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
587035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
587036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
587036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
587037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
587037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
587038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
587120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
587121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
587126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
587200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
587275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
587276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
587277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
587278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
587278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
587279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
587279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
587279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
587280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
587361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
587367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
587452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
587452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
587453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
587454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
587454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
587455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
587455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
587455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
587460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
587461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
587536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
587541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
587546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
587640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
587641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
587641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
587642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
587642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
587643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
587643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
587644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
587695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
587696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
587697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
587697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
587698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
587703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
587707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
587818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
587902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
587903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
587903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
587904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
588063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
588147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
588148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
591120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
591125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
591126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
591126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
591127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
591236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
591237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
591238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
591238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
591239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
591340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
594281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
597405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
597410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
597411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
597412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
597412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
597520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
597522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
597523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
597523     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)' ...' 
597525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
598643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
598643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
598643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.21s 
600856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
601591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
601592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.9ns 
601592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
601601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
601612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
601614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
601616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
601616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
601620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
601622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
601625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
601628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
601628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
601638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
601639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
601640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
601688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
601689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
601690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
601690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
601691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
601754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
601755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
601756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
601757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
601757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
601760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
601761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
601761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
601763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
601763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
601764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
601843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
601844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
601844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
601846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
601846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
601847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
601930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
601931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
601931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
601932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
601932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
601933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
601934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
601934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
601935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
601935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
601936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
601936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
601937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
601937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
601938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
601938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
601939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
601940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
601941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
601943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
601980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
601981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
602042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
602043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
602044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
602046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
602046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
602047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
602100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
602102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
602104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
602105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
602106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
602107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
602107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
602155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
602157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
602160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
602273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
602323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
602323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.7ns 
602323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.22s 
604539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
605295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
605326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.13ms