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

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

tests
0

failures
0

ignored
11m16.45s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.264s passed
powPositiveConcrete data()[101] 3.260s passed
powGeq1Concrete data()[102] 3.263s passed
pow2InIntLower data()[103] 3.255s passed
pow2InIntUpper data()[104] 3.260s passed
logSelfConcrete data()[105] 3.293s passed
log1Concrete data()[106] 3.276s passed
logProduct data()[107] 3.267s passed
logTimesBaseConcrete data()[108] 3.267s passed
logProdIdentity data()[109] 3.296s passed
moduloByteIsInByte data()[10] 3.357s passed
logProdIdentityConcrete data()[110] 3.276s passed
logPowIdentity data()[111] 3.303s passed
logPowIdentityConcrete data()[112] 3.280s passed
logPositive data()[113] 3.284s passed
logPositiveConcrete data()[114] 3.258s passed
logMono data()[115] 3.275s passed
logMonoConcrete data()[116] 3.261s passed
powLogLess data()[117] 3.310s passed
powLogMore2 data()[118] 3.319s passed
logLessThanPow data()[119] 3.300s passed
moduloCharIsInChar data()[11] 3.327s passed
logLessThanPowConcrete data()[120] 3.262s passed
logSqueeze data()[121] 3.265s passed
ifthenelse_equals data()[122] 3.260s passed
ifthenelse_equals_1 data()[123] 3.292s passed
ifthenelse_equals_2 data()[124] 3.265s passed
disjointWithSingleton1 data()[125] 3.273s passed
disjointWithSingleton2 data()[126] 3.260s passed
disjointArrayRanges data()[127] 3.293s passed
disjointArrayRangeAllFields1 data()[128] 3.284s passed
disjointArrayRangeAllFields2 data()[129] 3.263s passed
div_unique1 data()[12] 3.430s passed
seqSelfDefinition data()[130] 3.275s passed
seqOutsideValue data()[131] 3.291s passed
castedGetAny data()[132] 3.279s passed
seqGetAlphaCast data()[133] 3.284s passed
getOfSeqSingleton data()[134] 3.288s passed
getOfSeqSingletonConcrete data()[135] 3.290s passed
getOfSeqConcat data()[136] 3.277s passed
getOfSeqSub data()[137] 3.302s passed
getOfSeqReverse data()[138] 3.265s passed
lenOfSeqEmpty data()[139] 3.257s passed
div_unique2 data()[13] 3.440s passed
lenOfSeqSingleton data()[140] 3.293s passed
lenOfSeqConcat data()[141] 3.275s passed
lenOfSeqSub data()[142] 3.258s passed
lenOfSeqReverse data()[143] 3.298s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.266s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.282s passed
getOfSeqSingletonEQ data()[146] 3.259s passed
getOfSeqConcatEQ data()[147] 3.301s passed
getOfSeqSubEQ data()[148] 3.272s passed
getOfSeqReverseEQ data()[149] 3.277s passed
div_exists data()[14] 3.541s passed
lenOfSeqEmptyEQ data()[150] 3.296s passed
lenOfSeqSingletonEQ data()[151] 3.266s passed
lenOfSeqConcatEQ data()[152] 3.284s passed
lenOfSeqSubEQ data()[153] 3.283s passed
lenOfSeqReverseEQ data()[154] 3.284s passed
getOfSeqDefEQ data()[155] 3.271s passed
lenOfSeqDefEQ data()[156] 3.296s passed
seqConcatWithSeqEmpty1 data()[157] 3.304s passed
seqConcatWithSeqEmpty2 data()[158] 3.292s passed
seqReverseOfSeqEmpty data()[159] 3.296s passed
div_one data()[15] 3.321s passed
subSeqComplete data()[160] 3.274s passed
subSeqTailR data()[161] 3.307s passed
subSeqTailL data()[162] 3.308s passed
subSeqTailEQR data()[163] 3.295s passed
subSeqTailEQL data()[164] 3.303s passed
seqDef_split data()[165] 3.314s passed
seqDef_induction_upper data()[166] 3.341s passed
seqDef_induction_upper_concrete data()[167] 3.339s passed
seqDef_induction_lower data()[168] 3.330s passed
seqDef_induction_lower_concrete data()[169] 3.313s passed
jdiv_one data()[16] 3.322s passed
seqDef_split_in_three data()[170] 3.428s passed
seqDef_empty data()[171] 3.337s passed
seqDef_one_summand data()[172] 3.310s passed
seqDef_lower_equals_upper data()[173] 3.284s passed
seqDefOfSeq data()[174] 3.301s passed
seqSelfDefinitionEQ2 data()[175] 3.303s passed
indexOfSeqSingleton data()[176] 3.294s passed
indexOfSeqConcatFirst data()[177] 3.282s passed
indexOfSeqConcatSecond data()[178] 3.309s passed
indexOfSeqSub data()[179] 3.298s passed
div_zero data()[17] 3.334s passed
lenOfArray2seq data()[180] 3.301s passed
getAnyOfArray2seq data()[181] 3.297s passed
getOfArray2seq data()[182] 3.288s passed
getAnyOfNPermInv data()[183] 3.265s passed
seqNPermRange data()[184] 3.359s passed
seqPermTrans data()[185] 3.337s passed
seqPermRefl data()[186] 3.309s passed
seqPermSplit data()[187] 3.280s passed
seqNPermRight data()[188] 3.482s passed
seqPermFromSwap data()[189] 3.363s passed
divResZero1 data()[18] 3.371s passed
seqPermTransAlt0 data()[190] 3.290s passed
seqPermTransAlt1 data()[191] 3.294s passed
seqPermTransAlt2 data()[192] 3.284s passed
seqPermTransAlt3 data()[193] 3.287s passed
seqPermForall data()[194] 3.404s passed
seqPermExists data()[195] 3.344s passed
schiffl_lemma_2 data()[196] 22.866s passed
schiffl_thm_1 data()[197] 4.065s passed
eqSameSeq data()[198] 3.334s passed
divResZero2 data()[19] 3.343s passed
eqTermCut data()[1] 3.860s passed
divResOne1 data()[20] 3.365s passed
divResOne2 data()[21] 3.318s passed
div_cancel1 data()[22] 3.359s passed
div_cancel2 data()[23] 3.293s passed
divAddMultDenom data()[24] 3.328s passed
divMinus data()[25] 3.361s passed
divMinusDenom data()[26] 3.359s passed
divLeastDPos data()[27] 3.344s passed
divLeastDNeg data()[28] 3.328s passed
divGreatestDPos data()[29] 3.310s passed
equivAllRight data()[2] 3.711s passed
divGreatestDNeg data()[30] 3.296s passed
divIncreasingPos data()[31] 3.289s passed
divIncreasingNeg data()[32] 3.289s passed
jdiv_zero data()[33] 3.318s passed
jdivPulloutMinusNum data()[34] 3.314s passed
jdivPulloutMinusDenom data()[35] 3.332s passed
jdiv_uniquePosPos data()[36] 3.362s passed
jdiv_uniquePosNeg data()[37] 3.312s passed
jdiv_uniqueNegPos data()[38] 3.294s passed
jdiv_uniqueNegNeg data()[39] 3.289s passed
irrflConcrete1 data()[3] 3.545s passed
jdivMultDenom1 data()[40] 3.347s passed
jdivMultDenom2 data()[41] 3.268s passed
mod_geZero data()[42] 3.274s passed
mod_lessDenom data()[43] 3.287s passed
jmod_NumPos data()[44] 3.307s passed
jmod_NumNeg data()[45] 3.297s passed
jmod_geZero data()[46] 3.314s passed
jmodNumZero data()[47] 3.298s passed
jmod_pulloutminusNum data()[48] 3.297s passed
jmod_pulloutminusDenom data()[49] 3.285s passed
irrflConcrete2 data()[4] 3.507s passed
jmodUnique1 data()[50] 3.344s passed
jmodUnique2 data()[51] 3.369s passed
intDivRem data()[52] 3.282s passed
jmodjmod data()[53] 3.324s passed
jmodDivisible data()[54] 3.301s passed
jmodDivisibleRep data()[55] 3.295s passed
jdivAddMultDenom data()[56] 3.433s passed
jmodAltZero data()[57] 3.310s passed
jmodAddMultDenomZero data()[58] 3.308s passed
polyDiv_zero data()[59] 3.317s passed
cancel_gtPos data()[5] 3.526s passed
polyMod_ltdivDenom data()[60] 3.274s passed
bsum_empty data()[61] 3.272s passed
bsum_induction_upper data()[62] 3.266s passed
bsum_induction_lower data()[63] 3.291s passed
bsum_num_of_bounds data()[64] 3.315s passed
bsum_num_of_bounds2 data()[65] 3.286s passed
bsum_induction_upper2 data()[66] 3.301s passed
bsum_induction_upper_concrete data()[67] 3.272s passed
bsum_induction_upper_concrete_2 data()[68] 3.261s passed
bsum_induction_upper2_concrete data()[69] 3.262s passed
cancel_gtNeg data()[6] 3.435s passed
bsum_induction_lower_concrete data()[70] 3.267s passed
bsum_induction_lower2 data()[71] 3.264s passed
bsum_induction_lower2_concrete data()[72] 3.288s passed
bsum_positive data()[73] 3.305s passed
bsum_upper_bound data()[74] 3.298s passed
bsum_lower_bound data()[75] 3.309s passed
bsum_positive_lower_bound_element data()[76] 3.309s passed
bsum_sub_same_index data()[77] 3.297s passed
bsum_less_same_index data()[78] 3.355s passed
bsum_equal_except_one_index data()[79] 3.308s passed
moduloIntIsInInt data()[7] 3.451s passed
bsum_num_of_is_max data()[80] 3.322s passed
bsum_num_of_is_max2 data()[81] 3.299s passed
bsum_num_of_is_max3 data()[82] 3.309s passed
bsum_num_of_is_max4 data()[83] 3.315s passed
bsum_num_of_lt_max data()[84] 3.296s passed
bsum_num_of_lt_max2 data()[85] 3.330s passed
bsum_num_of_lt_max3 data()[86] 3.281s passed
bsum_num_of_lt_max4 data()[87] 3.287s passed
bsum_num_of_gt0 data()[88] 3.291s passed
bsum_num_of_gt0_alt data()[89] 3.306s passed
moduloLongIsInLong data()[8] 3.409s passed
bsum_add_concrete data()[90] 3.273s passed
bprod_all_positive data()[91] 3.302s passed
bprod_split data()[92] 3.279s passed
powConcrete0 data()[93] 3.277s passed
powConcrete1 data()[94] 3.281s passed
powSplitFactor data()[95] 3.293s passed
powAdd data()[96] 3.271s passed
powMono data()[97] 3.284s passed
powMonoConcrete data()[98] 3.298s passed
powMonoConcreteRight data()[99] 3.258s passed
moduloShortIsInShort data()[9] 3.382s passed

Standard output

584        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
608        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.9ms 
814        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
829        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)

1783       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1789       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1794       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1795       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3304       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8819       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8s 
8880       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8914       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.3ns 
8925       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8925       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.5ns 
8931       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11764      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
11766      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12778      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.54ms 
12788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12788      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.9ns 
12792      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15521      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
15521      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16496      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.38ms 
16499      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16499      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.2ns 
16501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19145      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
19145      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20035      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20042      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms 
20046      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20046      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 439.01ns 
20048      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22655      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
22655      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23544      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23550      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
23552      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23552      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127ns 
23553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26117      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
26117      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27074      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 72.95ms 
27081      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27082      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 745.62ns 
27084      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29671      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
29672      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30513      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.67ms 
30517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30517      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 424.71ns 
30518      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33094      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
33094      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33960      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33964      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 780.21ns 
33967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33968      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.21ns 
33969      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36544      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
36545      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37371      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37374      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.11ns 
37376      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37376      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.11ns 
37378      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
39914      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
40753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
40756      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 644.61ns 
40758      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
40758      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223ns 
40759      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43269      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
43270      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
44110      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
44113      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 657.21ns 
44115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
44116      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.01ns 
44117      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46607      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
46607      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
47437      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
47440      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.71ns 
47443      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
47443      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.41ns 
47445      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49975      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
49976      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
50780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
50867      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.18ms 
50876      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
50877      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 514.51ns 
50880      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53487      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
53487      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
54277      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
54312      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.76ms 
54319      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
54319      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 577.31ns 
54321      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56830      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
56830      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
57646      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
57852      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 197.82ms 
57856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
57856      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.2ns 
57857      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60353      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
60353      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
61169      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
61174      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
61175      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
61176      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135ns 
61176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63677      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
63678      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
64492      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
64496      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
64499      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
64499      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 283.81ns 
64500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66975      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
66976      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
67789      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
67830      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.66ms 
67833      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
67833      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.71ns 
67834      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70345      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
70346      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
71179      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
71202      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.97ms 
71204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
71204      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132ns 
71205      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73731      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
73732      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
74528      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
74544      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.83ms 
74547      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
74548      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.31ns 
74549      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77075      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
77076      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
77893      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
77910      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.26ms 
77912      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
77912      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.1ns 
77913      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80395      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
80395      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
81211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
81227      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.42ms 
81230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
81231      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 396.81ns 
81232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83741      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
83741      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
84562      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
84588      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.29ms 
84590      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
84590      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.1ns 
84591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87071      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
87071      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
87878      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
87881      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
87883      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
87883      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.1ns 
87884      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90350      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
90352      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
91167      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
91209      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.32ms 
91211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
91211      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.4ns 
91212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93723      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
93723      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
94513      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
94570      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.47ms 
94572      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
94572      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.6ns 
94573      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97093      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
97094      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
97883      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
97929      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.41ms 
97931      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
97931      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173ns 
97932      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
100441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
101253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
101271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.39ms 
101277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
101278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 867.22ns 
101280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
103776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
104589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
104602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.78ms 
104604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
104604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.1ns 
104605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
107090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
107900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
107912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.36ms 
107914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
107914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.1ns 
107915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
110391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
111199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
111208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.96ms 
111210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
111210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.31ns 
111211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
113684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
114488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
114497     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.09ms 
114499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
114499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.31ns 
114500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
116992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
117778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
117786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
117788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
117788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 248.1ns 
117789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
120292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
121100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
121104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
121105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
121105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.9ns 
121106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
123597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
124405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
124418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.76ms 
124419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
124420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.7ns 
124421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
126887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
127692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
127749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.33ms 
127753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
127763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.15ms 
127764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
130276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
131089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
131113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.77ms 
131114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
131115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.9ns 
131116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
133597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
134406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
134425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.29ms 
134427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
134427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136ns 
134428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
136915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
137700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
137719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16ms 
137721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
137721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
137722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
140203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
140990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
141007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.33ms 
141010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
141010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.81ns 
141011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
143511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
144314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
144354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.82ms 
144357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
144357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 359.71ns 
144359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
146813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
147619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
147622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
147625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
147625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.9ns 
147626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
150084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
150892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
150897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
150900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
150900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.11ns 
150901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
153371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
154177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
154185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.75ms 
154186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
154186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.7ns 
154187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
156678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
157483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
157492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.79ms 
157493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
157493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
157494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
159984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
160769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
160789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.43ms 
160790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
160790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.1ns 
160791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
163281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
164094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
164102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ms 
164104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
164104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.4ns 
164105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
166569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
167396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
167401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
167403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
167403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.81ns 
167404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
169884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
170692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
170697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
170699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
170700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.31ns 
170701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
173174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
173977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
173981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
173984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
173984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.9ns 
173985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
176450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
177257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
177326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.66ms 
177328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
177328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.3ns 
177329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
179828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
180613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
180695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.35ms 
180696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
180697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.6ns 
180697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
183191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
183973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
183977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
183979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
183979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.11ns 
183980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
186464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
187265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
187301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.65ms 
187304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
187304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 461.11ns 
187305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
189767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
190573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
190602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.51ms 
190604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
190605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.31ns 
190606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
193070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
193894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
193897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
193899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
193899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
193900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
196375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
197182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
197326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 134.02ms 
197332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
197332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.6ns 
197333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
199840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
200628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
200640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.05ms 
200643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
200643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.31ns 
200644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
203153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
203937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
203948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.01ms 
203950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
203950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
203950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
206439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
207247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
207265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.98ms 
207268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
207268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.1ns 
207269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
209726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
210526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
210538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.45ms 
210540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
210540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
210541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
213010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
213807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
213811     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
213812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
213812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
213813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
216269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
217072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
217077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
217078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
217078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
217079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
219537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
220343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
220368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.62ms 
220369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
220370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
220370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
222861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
223665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
223683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.38ms 
223684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
223685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
223685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
226170     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
226953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
226969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.64ms 
226971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
226971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
226972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
229464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
230267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
230271     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
230272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
230272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
230273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
232734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
233538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
233542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
233544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
233544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
233545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
235987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
236798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
236803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.75ms 
236805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
236805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
236806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
239257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
240061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
240065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
240067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
240067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.5ns 
240068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
242526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
243329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
243332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 736.11ns 
243334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
243335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.9ns 
243335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
245812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
246592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
246596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
246598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
246598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
246599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
249077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
249881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
249884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
249886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
249886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.8ns 
249887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
252336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
253138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
253189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.37ms 
253191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
253192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.31ns 
253193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
255644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
256445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
256488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.81ms 
256489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
256489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
256490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
258956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
259761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
259796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.32ms 
259798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
259798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
259799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
262249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
263054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
263105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.29ms 
263107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
263107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.1ns 
263108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
265589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
266369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
266402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.08ms 
266404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
266404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
266405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
268888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
269670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
269757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.11ms 
269763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
269764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.61ns 
269765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
272217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
273025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
273069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.39ms 
273071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
273071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
273072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
275567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
276370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
276391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.32ms 
276393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
276393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
276394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
278858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
279662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
279690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.02ms 
279692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
279692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.5ns 
279693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
282169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
282978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
282999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.07ms 
283001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
283001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
283001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
285504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
286286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
286314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.22ms 
286316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
286316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.9ns 
286317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
288802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
289581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
289610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.15ms 
289612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
289612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
289612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
292111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
292915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
292940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.08ms 
292941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
292942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.81ns 
292943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
295394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
296196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
296221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.03ms 
296222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
296223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
296223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
298684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
299487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
299508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.91ms 
299510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
299510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
299511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
301962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
302766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
302799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.92ms 
302801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
302801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
302802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
305298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
306080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
306105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.29ms 
306106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
306107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.1ns 
306107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
308588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
309370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
309379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.79ms 
309380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
309380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
309381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
311856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
312662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
312680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.7ms 
312682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
312682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
312683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
315150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
315956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
315960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
315961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
315961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
315962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
318426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
319234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
319237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 687.31ns 
319238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
319238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
319239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
321699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
322514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
322517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 853.32ns 
322519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
322519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
322520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
324998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
325802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
325810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
325812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
325812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
325812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
328294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
329075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
329081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
329083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
329083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
329083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
331571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
332353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
332365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.99ms 
332366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
332367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
332367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
334845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
335659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
335664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
335666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
335666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.5ns 
335667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
338118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
338919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
338921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 574.21ns 
338923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
338923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
338923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
341375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
342179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
342185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
342186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
342187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
342187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
344635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
345442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
345445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 726.41ns 
345451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
345451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.3ns 
345452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
347900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
348709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
348711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.71ns 
348712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
348712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
348713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
351183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
351964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
351966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.81ns 
351967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
351967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
351968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
354440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
355222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
355226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
355228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
355228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
355252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
357698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
358509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
358519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.25ms 
358521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
358521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
358521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
360984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
361791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
361795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
361796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
361796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
361797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
364249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
365054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
365062     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.13ms 
365063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
365063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
365064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
367520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
368324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
368329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
368330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
368330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
368331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
370816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
371603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
371625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.09ms 
371627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
371627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
371627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
374117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
374898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
374901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
374903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
374903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
374904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
377390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
378199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
378204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
378207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
378207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 195.1ns 
378208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
380672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
381480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
381485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
381486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
381486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
381487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
383947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
384751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
384768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.46ms 
384769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
384770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
384770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
387212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
388021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
388026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 553.71ns 
388028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
388028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.6ns 
388029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
390463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
391261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
391301     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.89ms 
391302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
391302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
391303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
393780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
394558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
394562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
394564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
394564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
394564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
397062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
397851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
397873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.08ms 
397874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
397874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
397875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
400364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
401170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
401191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.32ms 
401193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
401193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
401194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
403664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
404467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
404492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.49ms 
404493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
404493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
404494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
406946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
407751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
407753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 621.41ns 
407755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
407755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
407756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
410206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
411012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
411018     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
411020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
411020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
411020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
413492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
414275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
414279     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
414280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
414280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
414281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
416755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
417567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
417570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 928.52ns 
417572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
417572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
417572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
420026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
420833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
420835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 883.12ns 
420837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
420837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
420837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
423296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
424104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
424108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
424110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
424110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
424110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
426579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
427365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
427369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
427370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
427370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
427371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
429842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
430651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
430661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.73ms 
430662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
430662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
430663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
433121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
433932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
433945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.62ms 
433947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
433947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
433948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
436387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
437197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
437208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.12ms 
437209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
437209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
437210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
439681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
440471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
440484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.14ms 
440485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
440485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
440486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
442951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
443769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
443774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
443775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
443775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
443776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
446230     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
447047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
447053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.55ms 
447055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
447055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
447055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
449511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
450334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
450337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.91ns 
450338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
450338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
450339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
452807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
453622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
453626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
453627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
453627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
453628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
456099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
456913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
456916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 888.22ns 
456917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
456917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
456918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
459361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
460180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
460192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.06ms 
460194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
460194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
460195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
462674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
463490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
463494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 
463496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
463496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
463497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
465936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
466752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
466759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.16ms 
466760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
466760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
466761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
469200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
470014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
470017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 866.62ns 
470018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
470018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
470019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
472492     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
473307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
473309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 689.51ns 
473310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
473310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
473315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
475763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
476580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
476584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
476586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
476586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
476586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
479047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
479839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
479842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
479844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
479844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
479845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
482318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
483137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
483141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
483142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
483142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
483143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
485590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
486404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
486407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
486408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
486408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
486409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
488870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
489683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
489688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
489690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
489690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
489691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
492130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
492944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
492947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
492949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
492949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
492950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
495418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
496237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
496248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.12ms 
496249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
496249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
496250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
498700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
499518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
499521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 756.71ns 
499522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
499522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
499523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
501993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
502790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
502797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.39ms 
502798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
502798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
502799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
505275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
506091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
506093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
506095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
506095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
506095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
508565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
509357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
509360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 968.52ns 
509361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
509361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
509362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
511824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
512638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
512643     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
512644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
512644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
512645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
515124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
515923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
515926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
515927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
515927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
515928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
518391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
519207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
519210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
519212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
519212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
519212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
521685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
522477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
522481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
522482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
522482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
522483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
524957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
525772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
525778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.48ms 
525779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
525779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
525780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
528249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
529067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
529082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.97ms 
529083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
529083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
529084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
531539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
532357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
532373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.79ms 
532374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
532374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
532375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
534845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
535659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
535669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.78ms 
535671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
535671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
535672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
538117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
538932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
538943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.97ms 
538945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
538945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
538945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
541409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
542224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
542250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.32ms 
542252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
542252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
542253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
544711     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
545504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
545558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.2ms 
545560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
545560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
545561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
548011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
548829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
548853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.62ms 
548854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
548854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
548855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
551322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
552138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
552156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.98ms 
552157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
552157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
552158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
554624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
555422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
555470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.62ms 
555475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
555475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.8ns 
555476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
557947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
558765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
558813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.17ms 
558814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
558814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
558815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
561295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
562113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
562151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.18ms 
562153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
562153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
562154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
564623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
565439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
565481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.65ms 
565483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
565483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
565484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
567932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
568750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
568795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.48ms 
568796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
568796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
568797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
571279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
572097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
572222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 117.69ms 
572224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
572224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
572225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
574723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
575547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
575558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.3ms 
575563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
575563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
575564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
578046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
578862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
578870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
578871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
578871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.3ns 
578872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
581325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
582148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
582153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
582155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
582155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
582156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
584621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
585436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
585455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.55ms 
585456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
585456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
585457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
587928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
588746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
588757     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.99ms 
588758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
588759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
588759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
591228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
592048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
592052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
592053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
592053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
592054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
594497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
595315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
595333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.84ms 
595334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
595334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
595335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
597808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
598625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
598642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.47ms 
598644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
598644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
598645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
601106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
601921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
601940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.77ms 
601942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
601942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
601943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
604409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
605238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
605241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
605243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
605243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
605243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
607721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
608535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
608539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
608540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
608540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
608541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
611002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
611819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
611826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.21ms 
611827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
611827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
611828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
614269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
615082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
615091     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.53ms 
615093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
615093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.7ns 
615094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
617563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
618381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
618450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.75ms 
618452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
618452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
618453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
620944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
621760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
621787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.78ms 
621788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
621788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
621789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
624260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
625074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
625096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.81ms 
625098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
625098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
625099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
627556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
628374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
628376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 322.6ns 
628377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
628377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
628378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
630836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
631655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
631857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 191.87ms 
631860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
631860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.2ns 
631861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
634345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
635169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
635221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.44ms 
635222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
635222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
635223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
637691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
638509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
638511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 393.01ns 
638513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
638513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
638513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
640988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
641803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
641805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 397.01ns 
641807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
641808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.55ms 
641809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
644270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
645087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
645089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 400.31ns 
645090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
645091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
645091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
647554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
648374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
648376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 587.31ns 
648377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
648377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
648378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
650848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
651665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
651765     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
651780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 112.2ms 
651783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
651783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.91ns 
651785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
654256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
654256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
655073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
655122     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
655124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.23ms 
655126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
655126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
655127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
657590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
658409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
658410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ns 
658438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
658483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
658507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
658516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
658525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
658528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
658530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
658533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
658545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
658549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
658556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
658558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
658785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
658787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
658790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
658791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
658793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
658927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
658928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
658930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
658933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
658934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
658935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
659113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
659115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
659117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
659118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
659120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
659122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
659248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
659251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
659252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
659253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
659255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
659256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
659263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
659264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
659265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
659270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
659272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
659273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
659282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
659282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
659284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
659285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
659285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
659286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
659436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
659437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
659439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
659571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
659573     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)'' 
659576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
659577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
659578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
659579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
659580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
659583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
659587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
659589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
659590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
659591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
659592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
659715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
659720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
659722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
659722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
659724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
659725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
659727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
659891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
659893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
659894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
659896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
659896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
659897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
659897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
659898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
659996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
659998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
660085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
660089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
660093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
660094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
660095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
660096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
660097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
660097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
660098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
660099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
660108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
660113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
660200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
660202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
660203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
660204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
660204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
660205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
660205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
660206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
660253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
660258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
660339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
660343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
660345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
660346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
660347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
660348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
660462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
660467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
660468     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)'' 
660470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
660471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
660472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
660473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
660473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
660483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
660484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
660486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
660486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
660577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
660578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
660579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
660580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
660581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
660581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
660680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
660681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
660682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
660684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
660684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
660685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
660685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
660687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
660769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
660770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
660847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
660848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
660849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
660853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
660857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
660866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
660988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
660990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
660991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
660992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
661002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
661089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
664850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
664852     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)'' 
664857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
664859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
664859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
664860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
664862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
664870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
664872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
664873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
664874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
664874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
664975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
664980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
664981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
664982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
664983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
664984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
664984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
665084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
665086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
665087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
665090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
665090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
665091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
665092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
665093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
665179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
665181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
665260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
665265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
665269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
665270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
665271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
665272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
665282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
665366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
665367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
665368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
665369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
665450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
665460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
665461     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)'' 
665463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
665464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
665465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
665465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
665466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
665477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
665478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
665479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
665479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
665480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
665570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
665571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
665573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
665573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
665574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
665666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
665671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
665672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
665673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
665674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
665675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
665675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
665776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
665778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
665778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
665780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
665780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
665781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
665781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
665782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
665783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
665783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
665784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
665785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
665785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
665786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
665787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
665875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
665876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
665883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
665961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
666043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
666045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
666046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
666047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
666048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
666048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
666048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
666049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
666050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
666137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
666143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
666234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
666236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
666236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
666237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
666238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
666238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
666238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
666239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
666244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
666245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
666373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
666378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
666384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
666484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
666485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
666486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
666487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
666487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
666487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
666488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
666488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
666544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
666545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
666546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
666547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
666547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
666553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
666558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
666676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
666766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
666767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
666767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
666768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
666936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
667025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
667026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
670174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
670180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
670181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
670182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
670183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
670299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
670301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
670302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
670303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
670304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
670416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
673451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
676694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
676699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
676700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
676700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
676701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
676817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
676818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
676819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
676820     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)' ...' 
676822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
677992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
677992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 
677993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
680521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
681365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
681366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7ns 
681366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
681373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
681384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
681387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
681389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
681389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
681393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
681395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
681397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
681400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
681401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
681409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
681410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
681411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
681453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
681455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
681455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
681456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
681456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
681520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
681520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
681522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
681523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
681524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
681527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
681528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
681528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
681529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
681530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
681531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
681611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
681612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
681612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
681614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
681615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
681615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
681699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
681700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
681701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
681702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
681702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
681703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
681704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
681704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
681705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
681706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
681706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
681707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
681707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
681708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
681709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
681709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
681710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
681711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
681712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
681714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
681746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
681748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
681798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
681799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
681801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
681802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
681803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
681804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
681847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
681849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
681851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
681852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
681854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
681855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
681855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
681950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
681953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
681956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
682005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
682058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
682058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.91ns 
682059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
684510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
685356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
685389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.48ms