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

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

tests
0

failures
0

ignored
12m21.66s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.678s passed
powPositiveConcrete data()[101] 3.594s passed
powGeq1Concrete data()[102] 3.607s passed
pow2InIntLower data()[103] 3.534s passed
pow2InIntUpper data()[104] 3.573s passed
logSelfConcrete data()[105] 3.595s passed
log1Concrete data()[106] 3.545s passed
logProduct data()[107] 3.692s passed
logTimesBaseConcrete data()[108] 3.651s passed
logProdIdentity data()[109] 3.582s passed
moduloByteIsInByte data()[10] 3.662s passed
logProdIdentityConcrete data()[110] 3.548s passed
logPowIdentity data()[111] 3.546s passed
logPowIdentityConcrete data()[112] 3.535s passed
logPositive data()[113] 3.579s passed
logPositiveConcrete data()[114] 3.552s passed
logMono data()[115] 3.584s passed
logMonoConcrete data()[116] 3.540s passed
powLogLess data()[117] 3.593s passed
powLogMore2 data()[118] 3.585s passed
logLessThanPow data()[119] 3.650s passed
moduloCharIsInChar data()[11] 3.670s passed
logLessThanPowConcrete data()[120] 3.695s passed
logSqueeze data()[121] 3.588s passed
ifthenelse_equals data()[122] 3.583s passed
ifthenelse_equals_1 data()[123] 3.549s passed
ifthenelse_equals_2 data()[124] 3.579s passed
disjointWithSingleton1 data()[125] 3.582s passed
disjointWithSingleton2 data()[126] 3.550s passed
disjointArrayRanges data()[127] 3.579s passed
disjointArrayRangeAllFields1 data()[128] 3.613s passed
disjointArrayRangeAllFields2 data()[129] 3.708s passed
div_unique1 data()[12] 3.795s passed
seqSelfDefinition data()[130] 3.641s passed
seqOutsideValue data()[131] 3.574s passed
castedGetAny data()[132] 3.628s passed
seqGetAlphaCast data()[133] 3.566s passed
getOfSeqSingleton data()[134] 3.568s passed
getOfSeqSingletonConcrete data()[135] 3.580s passed
getOfSeqConcat data()[136] 3.576s passed
getOfSeqSub data()[137] 3.565s passed
getOfSeqReverse data()[138] 3.593s passed
lenOfSeqEmpty data()[139] 3.610s passed
div_unique2 data()[13] 3.862s passed
lenOfSeqSingleton data()[140] 3.618s passed
lenOfSeqConcat data()[141] 3.556s passed
lenOfSeqSub data()[142] 3.622s passed
lenOfSeqReverse data()[143] 3.616s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.584s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.561s passed
getOfSeqSingletonEQ data()[146] 3.618s passed
getOfSeqConcatEQ data()[147] 3.588s passed
getOfSeqSubEQ data()[148] 3.589s passed
getOfSeqReverseEQ data()[149] 3.578s passed
div_exists data()[14] 3.835s passed
lenOfSeqEmptyEQ data()[150] 3.563s passed
lenOfSeqSingletonEQ data()[151] 3.593s passed
lenOfSeqConcatEQ data()[152] 3.549s passed
lenOfSeqSubEQ data()[153] 3.719s passed
lenOfSeqReverseEQ data()[154] 3.563s passed
getOfSeqDefEQ data()[155] 3.593s passed
lenOfSeqDefEQ data()[156] 3.586s passed
seqConcatWithSeqEmpty1 data()[157] 3.601s passed
seqConcatWithSeqEmpty2 data()[158] 3.635s passed
seqReverseOfSeqEmpty data()[159] 3.610s passed
div_one data()[15] 3.618s passed
subSeqComplete data()[160] 3.646s passed
subSeqTailR data()[161] 3.606s passed
subSeqTailL data()[162] 3.609s passed
subSeqTailEQR data()[163] 3.620s passed
subSeqTailEQL data()[164] 3.586s passed
seqDef_split data()[165] 3.615s passed
seqDef_induction_upper data()[166] 3.643s passed
seqDef_induction_upper_concrete data()[167] 3.637s passed
seqDef_induction_lower data()[168] 3.719s passed
seqDef_induction_lower_concrete data()[169] 3.695s passed
jdiv_one data()[16] 3.552s passed
seqDef_split_in_three data()[170] 3.792s passed
seqDef_empty data()[171] 3.629s passed
seqDef_one_summand data()[172] 3.622s passed
seqDef_lower_equals_upper data()[173] 3.610s passed
seqDefOfSeq data()[174] 3.585s passed
seqSelfDefinitionEQ2 data()[175] 3.620s passed
indexOfSeqSingleton data()[176] 3.616s passed
indexOfSeqConcatFirst data()[177] 3.684s passed
indexOfSeqConcatSecond data()[178] 3.658s passed
indexOfSeqSub data()[179] 3.716s passed
div_zero data()[17] 3.666s passed
lenOfArray2seq data()[180] 3.626s passed
getAnyOfArray2seq data()[181] 3.582s passed
getOfArray2seq data()[182] 3.603s passed
getAnyOfNPermInv data()[183] 3.603s passed
seqNPermRange data()[184] 3.699s passed
seqPermTrans data()[185] 3.680s passed
seqPermRefl data()[186] 3.685s passed
seqPermSplit data()[187] 3.649s passed
seqNPermRight data()[188] 3.864s passed
seqPermFromSwap data()[189] 3.654s passed
divResZero1 data()[18] 3.649s passed
seqPermTransAlt0 data()[190] 3.585s passed
seqPermTransAlt1 data()[191] 3.681s passed
seqPermTransAlt2 data()[192] 3.694s passed
seqPermTransAlt3 data()[193] 3.563s passed
seqPermForall data()[194] 3.703s passed
seqPermExists data()[195] 3.692s passed
schiffl_lemma_2 data()[196] 26.110s passed
schiffl_thm_1 data()[197] 4.423s passed
eqSameSeq data()[198] 3.694s passed
divResZero2 data()[19] 3.619s passed
eqTermCut data()[1] 4.426s passed
divResOne1 data()[20] 3.593s passed
divResOne2 data()[21] 3.655s passed
div_cancel1 data()[22] 3.674s passed
div_cancel2 data()[23] 3.594s passed
divAddMultDenom data()[24] 3.622s passed
divMinus data()[25] 3.687s passed
divMinusDenom data()[26] 3.620s passed
divLeastDPos data()[27] 3.548s passed
divLeastDNeg data()[28] 3.624s passed
divGreatestDPos data()[29] 3.605s passed
equivAllRight data()[2] 4.085s passed
divGreatestDNeg data()[30] 3.606s passed
divIncreasingPos data()[31] 3.588s passed
divIncreasingNeg data()[32] 3.640s passed
jdiv_zero data()[33] 3.597s passed
jdivPulloutMinusNum data()[34] 3.574s passed
jdivPulloutMinusDenom data()[35] 3.632s passed
jdiv_uniquePosPos data()[36] 3.643s passed
jdiv_uniquePosNeg data()[37] 3.615s passed
jdiv_uniqueNegPos data()[38] 3.586s passed
jdiv_uniqueNegNeg data()[39] 3.572s passed
irrflConcrete1 data()[3] 3.956s passed
jdivMultDenom1 data()[40] 3.580s passed
jdivMultDenom2 data()[41] 3.528s passed
mod_geZero data()[42] 3.572s passed
mod_lessDenom data()[43] 3.578s passed
jmod_NumPos data()[44] 3.533s passed
jmod_NumNeg data()[45] 3.599s passed
jmod_geZero data()[46] 3.562s passed
jmodNumZero data()[47] 3.665s passed
jmod_pulloutminusNum data()[48] 3.547s passed
jmod_pulloutminusDenom data()[49] 3.528s passed
irrflConcrete2 data()[4] 3.757s passed
jmodUnique1 data()[50] 3.646s passed
jmodUnique2 data()[51] 3.654s passed
intDivRem data()[52] 3.566s passed
jmodjmod data()[53] 3.617s passed
jmodDivisible data()[54] 3.566s passed
jmodDivisibleRep data()[55] 3.545s passed
jdivAddMultDenom data()[56] 3.694s passed
jmodAltZero data()[57] 3.562s passed
jmodAddMultDenomZero data()[58] 3.544s passed
polyDiv_zero data()[59] 3.601s passed
cancel_gtPos data()[5] 3.819s passed
polyMod_ltdivDenom data()[60] 3.542s passed
bsum_empty data()[61] 3.537s passed
bsum_induction_upper data()[62] 3.564s passed
bsum_induction_lower data()[63] 3.586s passed
bsum_num_of_bounds data()[64] 3.616s passed
bsum_num_of_bounds2 data()[65] 3.653s passed
bsum_induction_upper2 data()[66] 3.562s passed
bsum_induction_upper_concrete data()[67] 3.578s passed
bsum_induction_upper_concrete_2 data()[68] 3.664s passed
bsum_induction_upper2_concrete data()[69] 3.640s passed
cancel_gtNeg data()[6] 3.733s passed
bsum_induction_lower_concrete data()[70] 3.564s passed
bsum_induction_lower2 data()[71] 3.569s passed
bsum_induction_lower2_concrete data()[72] 3.578s passed
bsum_positive data()[73] 3.671s passed
bsum_upper_bound data()[74] 3.704s passed
bsum_lower_bound data()[75] 3.678s passed
bsum_positive_lower_bound_element data()[76] 3.688s passed
bsum_sub_same_index data()[77] 3.614s passed
bsum_less_same_index data()[78] 3.622s passed
bsum_equal_except_one_index data()[79] 3.640s passed
moduloIntIsInInt data()[7] 3.678s passed
bsum_num_of_is_max data()[80] 3.591s passed
bsum_num_of_is_max2 data()[81] 3.639s passed
bsum_num_of_is_max3 data()[82] 3.581s passed
bsum_num_of_is_max4 data()[83] 3.607s passed
bsum_num_of_lt_max data()[84] 3.548s passed
bsum_num_of_lt_max2 data()[85] 3.616s passed
bsum_num_of_lt_max3 data()[86] 3.669s passed
bsum_num_of_lt_max4 data()[87] 3.642s passed
bsum_num_of_gt0 data()[88] 3.715s passed
bsum_num_of_gt0_alt data()[89] 3.709s passed
moduloLongIsInLong data()[8] 3.711s passed
bsum_add_concrete data()[90] 3.621s passed
bprod_all_positive data()[91] 3.632s passed
bprod_split data()[92] 3.547s passed
powConcrete0 data()[93] 3.546s passed
powConcrete1 data()[94] 3.562s passed
powSplitFactor data()[95] 3.597s passed
powAdd data()[96] 3.693s passed
powMono data()[97] 3.604s passed
powMonoConcrete data()[98] 3.591s passed
powMonoConcreteRight data()[99] 3.537s passed
moduloShortIsInShort data()[9] 3.754s passed

Standard output

447        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
474        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.77ms 
710        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
728        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)

1808       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1810       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1812       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1813       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3683       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9602       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.89s 
9684       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9726       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.5ns 
9742       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9745       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.07ms 
9751       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13054      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
13058      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14130      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14158      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.53ms 
14175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14175      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.71ns 
14177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17242      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
17242      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
18241      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
18257      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
18260      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
18260      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.52ns 
18262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21186      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
21186      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
22205      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
22213      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
22218      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
22218      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 439.82ns 
22220      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25030      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
25031      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
25967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
25973      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.08ms 
25978      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
25979      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 590.73ns 
25980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28754      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
28755      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
29720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
29793      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.77ms 
29795      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
29795      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.71ns 
29796      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32612      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
32613      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
33501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
33525      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.27ms 
33530      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
33530      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 443.32ns 
33532      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36310      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
36311      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
37202      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
37206      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 749.74ns 
37209      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
37209      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.62ns 
37210      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39943      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
39943      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
40909      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
40917      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 661.34ns 
40919      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
40920      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.33ms 
40921      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43752      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
43752      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
44668      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
44671      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 781.94ns 
44672      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
44673      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.91ns 
44674      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47417      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
47417      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
48327      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
48330      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 706.84ns 
48336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
48336      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.21ns 
48337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51066      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
51066      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
52001      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
52004      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
52006      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
52007      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 584.93ns 
52008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54721      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
54722      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
55664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
55799      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 120.05ms 
55803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
55807      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.03ms 
55808      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58730      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
58731      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
59618      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
59663      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.02ms 
59666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
59666      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.32ns 
59668      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62420      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
62421      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
63298      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
63497      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 190.19ms 
63501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
63501      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.11ns 
63502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66204      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
66204      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
67111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
67117      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.63ms 
67120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
67121      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.42ns 
67122      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69763      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
69765      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
70666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
70670      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
70675      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
70675      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 402.12ns 
70677      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73379      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
73380      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
74283      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
74337      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.41ms 
74341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
74342      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.51ns 
74343      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77062      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
77062      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
77970      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
77989      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.12ms 
77990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
77990      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.21ns 
77991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80686      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
80686      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
81591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
81607      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.97ms 
81610      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
81611      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.42ns 
81612      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84304      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
84304      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
85181      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
85200      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.26ms 
85202      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
85204      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.31ns 
85205      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87963      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
87963      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
88839      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
88856      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.06ms 
88858      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
88858      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.81ns 
88859      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91561      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
91561      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
92502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
92530      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.24ms 
92533      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
92533      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.02ns 
92534      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95220      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
95220      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
96120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
96124      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
96126      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
96127      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.12ns 
96128      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98793      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
98794      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
99685      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
99746      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.83ms 
99751      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
99751      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.82ns 
99753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
102475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
103375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
103436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.66ms 
103438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
103438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.11ns 
103439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
106111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
107009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
107055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.53ms 
107057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
107057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.91ns 
107058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
109740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
110595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
110604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.33ms 
110605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
110606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.81ns 
110607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
113338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
114215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
114228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.95ms 
114230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
114230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.21ns 
114231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
116950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
117822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
117834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.46ms 
117835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
117835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.41ns 
117836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
120525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
121431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
121439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
121440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
121441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.51ns 
121441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
124133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
125019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
125027     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.96ms 
125028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
125029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.61ns 
125030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
127713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
128659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
128667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ms 
128668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
128669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.61ns 
128670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
131357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
132260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
132264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
132266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
132266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.31ns 
132267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
134958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
135827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
135838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.63ms 
135839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
135839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.11ns 
135841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
138555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
139415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
139469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.82ms 
139473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
139473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.82ns 
139474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
142198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
143095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
143114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.39ms 
143117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
143117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.52ns 
143118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
145796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
146711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
146729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms 
146731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
146731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.01ns 
146732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
149406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
150296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
150315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.52ms 
150316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
150316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.61ns 
150317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
152978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
153870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
153887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.03ms 
153889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
153889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.61ns 
153890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
156536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
157426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
157467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.69ms 
157468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
157468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.81ns 
157469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
160126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
160992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
160995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
160996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
160996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
160997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
163692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
164563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
164568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
164569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
164569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.61ns 
164570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
167271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
168129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
168142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.39ms 
168148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
168151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.22ms 
168152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
170785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
171670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
171678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.25ms 
171680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
171680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.31ns 
171681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
174360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
175258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
175278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.49ms 
175279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
175279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.51ns 
175280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
177937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
178831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
178839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.41ms 
178841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
178841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.61ns 
178842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
181501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
182500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
182503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
182506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
182506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.71ns 
182507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
185188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
186047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
186051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
186053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
186053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.41ns 
186054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
188718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
189575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
189580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.22ms 
189581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
189581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
189582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
192228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
193134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
193225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.44ms 
193227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
193227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
193228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
195879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
196795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
196879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.01ms 
196881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
196881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.31ns 
196882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
199542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
200442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
200445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.61ms 
200447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
200447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.11ns 
200448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
203129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
204016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
204062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.93ms 
204064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
204064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.51ns 
204065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
206708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
207597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
207628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.43ms 
207630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
207630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
207631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
210308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
211169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
211172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
211179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
211179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.51ns 
211181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
213853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
214709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
214867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 146.6ms 
214870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
214870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.51ns 
214871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
217562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
218418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
218430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.64ms 
218433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
218434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.12ns 
218435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
221079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
221964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
221974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ms 
221976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
221976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.41ns 
221976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
224668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
225557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
225576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.29ms 
225577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
225577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
225578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
228212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
229097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
229115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ms 
229119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
229120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.92ns 
229121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
231775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
232651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
232655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
232657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
232657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138.31ns 
232658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
235328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
236215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
236220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
236221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
236221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
236222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
238910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
239780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
239805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.39ms 
239807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
239807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.81ns 
239808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
242534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
243403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
243421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.76ms 
243423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
243423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.41ns 
243424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
246160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
247056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
247074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.07ms 
247076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
247077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.52ns 
247078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
249736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
250633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
250637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
250638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
250638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
250639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
253314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
254209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
254214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.94ms 
254215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
254216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
254216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
256907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
257871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
257878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
257879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
257880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.61ns 
257880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
260614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
261514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
261518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
261520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
261520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.11ns 
261521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
264215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
265080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
265082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 792.54ns 
265083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
265083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
265084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
267779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
268646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
268651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
268652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
268652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
268653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
271313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
272225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
272228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
272231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
272231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.31ns 
272232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
274905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
275808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
275900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 88.92ms 
275904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
275904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.92ns 
275912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
278649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
279553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
279603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.79ms 
279606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
279606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.91ns 
279607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
282286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
283236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
283282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.98ms 
283285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
283285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 260.71ns 
283286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
286002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
286912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
286970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.28ms 
286972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
286972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.21ns 
286973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
289679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
290545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
290584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.33ms 
290586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
290587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 274.82ns 
290588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
293276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
294136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
294206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.37ms 
294208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
294208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.81ns 
294209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
296922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
297814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
297846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.97ms 
297848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
297848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
297848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
300524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
301414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
301438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.55ms 
301439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
301439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
301440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
304111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
305019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
305076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.13ms 
305078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
305078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
305079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
307738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
308634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
308657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.9ms 
308659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
308659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
308660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
311333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
312233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
312264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.14ms 
312266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
312266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
312266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
314931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
315784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
315812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.61ms 
315814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
315814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.61ns 
315815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
318527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
319398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
319428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.05ms 
319429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
319430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
319430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
322142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
323064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
323096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.29ms 
323098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
323099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
323099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
325816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
326711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
326739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.19ms 
326741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
326741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.11ns 
326742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
329517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
330416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
330454     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.97ms 
330455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
330456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.61ns 
330457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
333217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
334132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
334163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.83ms 
334164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
334164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.11ns 
334165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
336879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
337768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
337784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ms 
337787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
337787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 446.03ns 
337788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
340470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
341391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
341417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.03ms 
341420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
341421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.63ns 
341422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
344095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
344960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
344965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
344966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
344966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.21ns 
344967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
347645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
348508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
348511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 840.57ns 
348512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
348512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.01ns 
348513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
351185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
352071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
352074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 875.35ns 
352075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
352075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
352076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
354757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
355662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
355670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.61ms 
355672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
355672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
355673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
358378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
359353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
359363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.76ms 
359367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
359375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.43ms 
359376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
362051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
362954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
362969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.72ms 
362970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
362970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.31ns 
362971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
365631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
366555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
366559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
366560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
366560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
366561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
369225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
370094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
370096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 640.65ns 
370097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
370098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
370098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
372874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
373768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
373774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
373775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
373775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.81ns 
373776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
376470     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
377366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
377368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 739.36ns 
377369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
377370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
377370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
380069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
380973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
380975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 697.86ns 
380976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
380976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.51ns 
380977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
383626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
384507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
384510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 665.25ns 
384511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
384511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
384512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
387177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
388078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
388082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
388083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
388084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.51ns 
388084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
390780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
391667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
391677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.81ms 
391678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
391678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.71ns 
391679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
394355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
395218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
395222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
395224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
395224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.61ns 
395225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
397979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
398907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
398915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
398916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
398916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
398917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
401606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
402551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
402562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.07ms 
402567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
402567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 299.72ns 
402568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
405238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
406130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
406147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.92ms 
406149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
406149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.41ns 
406150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
408802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
409692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
409696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
409697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
409697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
409698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
412351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
413237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
413241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
413242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
413242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.41ns 
413243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
415896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
416770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
416777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ms 
416778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
416778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
416779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
419467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
420336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
420355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.89ms 
420357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
420357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
420357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
423047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
423901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
423906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 672.35ns 
423910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
423910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.62ns 
423911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
426559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
427449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
427492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.01ms 
427494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
427494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.81ns 
427495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
430124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
431029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
431032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
431034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
431034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.11ns 
431035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
433709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
434601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
434625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.39ms 
434627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
434627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.01ns 
434628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
437300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
438187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
438210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.13ms 
438212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
438212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.11ns 
438213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
440885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
441827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
441860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.65ms 
441862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
441862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.11ns 
441869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
444684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
445553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
445556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 754.46ns 
445557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
445557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.11ns 
445558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
448267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
449137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
449143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.54ms 
449145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
449145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
449146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
451834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
452723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
452726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
452728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
452728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.41ns 
452728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
455383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
456272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
456275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 876.16ns 
456276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
456277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
456277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
458951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
459851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
459854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 951.56ns 
459855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
459856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
459856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
462529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
463433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
463437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
463438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
463438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
463439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
466109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
466984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
466987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
466988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
466988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
466990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
469684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
470554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
470565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.87ms 
470567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
470567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
470568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
473294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
474165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
474178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.11ms 
474179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
474180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.11ns 
474180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
476960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
477874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
477886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.79ms 
477888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
477889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.22ns 
477889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
480593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
481501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
481527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.48ms 
481529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
481530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.62ns 
481531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
484189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
485097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
485102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.22ms 
485103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
485103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.41ns 
485104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
487805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
488720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
488730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.53ms 
488731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
488731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.51ns 
488732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
491415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
492293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
492296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 842.16ns 
492297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
492297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.61ns 
492298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
494985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
495860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
495863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
495865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
495865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.41ns 
495865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
498558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
499440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
499443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 945.07ns 
499444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
499444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
499445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
502102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
503007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
503020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.82ms 
503021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
503021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.31ns 
503022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
505673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
506580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
506585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.97ms 
506586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
506586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.11ns 
506587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
509265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
510169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
510177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
510179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
510179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.22ns 
510180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
512854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
513784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
513787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 952.07ns 
513789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
513789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.11ns 
513790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
516457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
517403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
517405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 813.26ns 
517406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
517406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.41ns 
517407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
520076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
520957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
520961     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
520962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
520963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.11ns 
520963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
523718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
524580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
524584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
524585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
524585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
524586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
527295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
528195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
528199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
528200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
528200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
528201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
530902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
531780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
531783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
531784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
531785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
531785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
534429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
535339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
535344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.13ms 
535346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
535346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
535347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
538047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
538959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
538962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
538964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
538964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
538964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
541634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
542538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
542550     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.65ms 
542552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
542553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.31ns 
542554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
545217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
546137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
546139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.16ns 
546141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
546141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
546141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
548800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
549709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
549717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.84ms 
549719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
549719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
549720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
552368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
553277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
553280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
553281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
553281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
553282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
555954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
556871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
556874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 903.76ns 
556875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
556875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.41ns 
556876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
559518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
560417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
560423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
560424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
560424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.11ns 
560425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
563178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
564136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
564141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
564143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
564143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.32ns 
564144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
566790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
567700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
567704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
567705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
567705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
567706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
570385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
571293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
571298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
571299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
571299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
571300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
573966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
574878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
574883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.72ms 
574884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
574885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
574885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
577553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
578468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
578484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.14ms 
578486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
578486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.11ns 
578486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
581183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
582102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
582119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.43ms 
582121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
582121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.61ns 
582122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
584806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
585718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
585729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.94ms 
585731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
585731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.31ns 
585732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
588422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
589363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
589376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.26ms 
589377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
589377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
589378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
592042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
592952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
592981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.3ms 
592983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
592983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.91ns 
592984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
595678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
596562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
596591     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.35ms 
596592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
596592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.11ns 
596593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
599296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
600182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
600210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.18ms 
600212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
600212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
600212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
602902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
603780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
603796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.9ms 
603797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
603797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.61ns 
603798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
606469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
606469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
607377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
607412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.09ms 
607413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
607413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
607414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
610099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
611002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
611054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.45ms 
611056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
611056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
611057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
613737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
614647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
614691     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.13ms 
614694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
614694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.72ns 
614695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
617409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
618362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
618410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.98ms 
618412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
618412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.71ns 
618413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
621137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
622054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
622105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.19ms 
622106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
622107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.91ns 
622108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
624878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
625761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
625897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 130.05ms 
625899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
625899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.91ns 
625900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
628623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
629512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
629526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.11ms 
629528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
629528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
629529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
632234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
633140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
633148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.49ms 
633151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
633151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.71ns 
633152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
635836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
636752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
636758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms 
636759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
636759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
636760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
639414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
640323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
640343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.46ms 
640345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
640345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
640345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
643031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
643951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
643964     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.34ms 
643965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
643965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
643966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
646669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
647576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
647579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
647581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
647581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.31ns 
647581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
650289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
651244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
651263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.03ms 
651265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
651265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.81ns 
651265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
653955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
654902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
654921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.41ms 
654922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
654922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
654923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
657665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
658613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
658637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.07ms 
658639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
658639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.22ns 
658640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
661346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
662260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
662264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
662265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
662265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
662266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
664956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
665841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
665846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
665847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
665847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
665848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
668531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
669442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
669449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.09ms 
669450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
669450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.41ns 
669451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
672128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
673045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
673052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.66ms 
673053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
673053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.11ns 
673054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
675739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
676658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
676750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 84.94ms 
676752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
676752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.81ns 
676753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
679472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
680393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
680429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.44ms 
680432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
680432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.51ns 
680433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
683179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
684090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
684115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.47ms 
684117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
684117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.11ns 
684117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
686851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
687762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
687764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 325.82ns 
687765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
687765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
687767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
690468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
690468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
691357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
691627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 259.15ms 
691630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
691630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.11ns 
691631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
694304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
695222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
695282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.8ms 
695283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
695284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.41ns 
695284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.67s 
697952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
698865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
698867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 425.72ns 
698868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
698869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
698869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
701627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
702546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
702549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 411.63ns 
702550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
702550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
702551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
705323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
706240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
706242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 404.52ns 
706244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
706245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.25ms 
706246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
708895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
709802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
709805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 552.53ns 
709806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
709806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
709807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
712496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
713408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
713507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 97.55ms 
713510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
713510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.93ns 
713511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
716229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
717143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
717200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.43ms 
717202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
717202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
717204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
720002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
720895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
720897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ns 
720927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
720985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
721004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
721009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
721015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
721018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
721019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
721022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
721025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
721027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
721029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
721030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
721201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
721203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
721204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
721206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
721207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
721333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
721335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
721336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
721339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
721340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
721341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
721586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
721587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
721588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
721589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
721590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
721591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
721747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
721749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
721751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
721752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
721753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
721754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
721763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
721766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
721766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
721769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
721771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
721772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
721783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
721784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
721785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
721786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
721787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
721788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
721960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
721962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
721964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
722126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
722128     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)'' 
722131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
722132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
722134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
722136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
722137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
722140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
722144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
722147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
722148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
722149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
722150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
722280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
722285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
722286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
722287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
722288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
722289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
722291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
722442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
722443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
722444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
722446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
722447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
722447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
722448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
722449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
722578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
722580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
722716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
722722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
722728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
722729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
722730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
722731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
722734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
722735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
722735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
722737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
722747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
722752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
722873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
722875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
722877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
722878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
722879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
722879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
722880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
722881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
723000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
723009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
723146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
723148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
723150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
723152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
723152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
723153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
723305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
723309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
723312     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)'' 
723315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
723317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
723318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
723319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
723319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
723329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
723335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
723337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
723338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
723442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
723443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
723444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
723446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
723446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
723447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
723558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
723560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
723561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
723563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
723564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
723565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
723566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
723567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
723657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
723660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
723743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
723743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
723744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
723749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
723754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
723759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
723893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
723894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
723897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
723898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
723910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
724007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
728167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
728168     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)'' 
728175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
728176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
728177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
728177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
728178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
728187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
728189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
728190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
728192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
728193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
728301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
728306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
728307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
728308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
728309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
728309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
728310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
728419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
728420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
728421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
728423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
728423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
728424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
728425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
728426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
728515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
728516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
728604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
728608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
728614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
728615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
728616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
728617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
728628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
728725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
728727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
728728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
728729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
728814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
728825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
728826     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)'' 
728828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
728829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
728830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
728831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
728832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
728844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
728846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
728847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
728848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
728849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
728953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
728954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
728956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
728957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
728958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
729064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
729070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
729071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
729072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
729073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
729074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
729074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
729191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
729192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
729193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
729195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
729196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
729197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
729197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
729199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
729200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
729201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
729202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
729203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
729203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
729204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
729205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
729308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
729310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
729317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
729407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
729504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
729506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
729508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
729509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
729510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
729510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
729511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
729512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
729513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
729616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
729623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
729731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
729733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
729734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
729735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
729736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
729737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
729737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
729738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
729745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
729746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
729840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
729847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
729853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
729973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
729975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
729976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
729977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
729977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
729978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
729979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
729980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
730045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
730046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
730047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
730048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
730049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
730056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
730063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
730203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
730310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
730311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
730312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
730314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
730585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
730690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
730691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
734242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
734248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
734249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
734250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
734251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
734382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
734384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
734385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
734386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
734387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
734512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
738012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
741814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
741820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
741821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
741822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
741823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
741957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
741958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
741959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
741960     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)' ...' 
741962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
743312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
743312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.31ns 
743313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
746020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
746020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
746964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
746966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
746966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
746975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
746988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
746991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
746993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
746993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
746998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
746999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
747003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
747006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
747006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
747016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
747018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
747019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
747070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
747072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
747072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
747073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
747073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
747142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
747143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
747144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
747145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
747146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
747150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
747150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
747151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
747152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
747153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
747154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
747241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
747242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
747242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
747244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
747245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
747246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
747339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
747340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
747341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
747342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
747342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
747344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
747344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
747345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
747346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
747346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
747347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
747348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
747348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
747349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
747350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
747350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
747351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
747352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
747353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
747356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
747398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
747399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
747466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
747467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
747469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
747470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
747471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
747472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
747531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
747534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
747536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
747538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
747539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
747540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
747540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
747596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
747599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
747603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
747667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
747735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
747735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.92ns 
747736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
750447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
750448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
751392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
751428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.39ms