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

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

tests
0

failures
0

ignored
11m16.41s

duration
100%

successful

Tests

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

Standard output

355        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
384        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.51ms 
603        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616        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)

1501       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1503       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1508       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1508       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2856       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8470       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.87s 
8584       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8617       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.9ns 
8633       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8633       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 513.01ns 
8638       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11625      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
11628      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12608      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.5ms 
12625      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12625      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 468.11ns 
12628      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15454      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
15455      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16317      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.76ms 
16320      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16322      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.52ms 
16324      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19052      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
19053      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19968      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19978      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.23ms 
19983      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19984      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155ns 
19988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22576      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
22577      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23454      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23459      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
23461      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23461      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.8ns 
23462      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26069      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
26069      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26904      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26945      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.8ms 
26947      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26947      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.6ns 
26948      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
29499      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30372      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.03ms 
30379      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30380      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.91ns 
30381      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32916      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
32916      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33751      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33755      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 698.41ns 
33757      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33758      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.2ns 
33759      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36376      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
36376      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37183      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 661.41ns 
37186      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37186      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.31ns 
37187      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39727      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
39728      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
40551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
40554      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.31ns 
40556      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
40557      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.4ns 
40558      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43064      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
43064      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43887      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43890      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.11ns 
43892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43892      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
43893      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46442      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
46442      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
47239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
47242      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 648.81ns 
47245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
47246      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.41ns 
47247      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49849      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
49849      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
50669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
50710      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.54ms 
50714      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
50714      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.2ns 
50720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53218      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
53218      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
54042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
54112      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.19ms 
54114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
54114      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.8ns 
54115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56641      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
56641      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
57438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
57591      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 144.07ms 
57595      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
57595      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 389.3ns 
57596      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60121      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
60121      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
60939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
60944      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
60946      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
60946      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201ns 
60947      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63435      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
63436      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
64260      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
64263      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
64266      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
64267      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313ns 
64268      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66787      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
66788      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
67582      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
67620      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.98ms 
67622      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
67622      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 
67623      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70131      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
70131      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
70948      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
70964      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.34ms 
70966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
70967      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.4ns 
70968      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73448      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
73448      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
74268      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
74282      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.39ms 
74283      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
74284      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.9ns 
74284      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76789      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
76789      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
77581      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
77601      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.85ms 
77603      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
77603      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.3ns 
77604      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80136      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
80136      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
80953      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
80967      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.72ms 
80969      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
80969      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.3ns 
80970      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83451      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
83451      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
84287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
84315      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.15ms 
84318      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
84318      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.21ns 
84319      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86831      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
86831      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
87623      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
87626      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
87628      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
87628      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108ns 
87629      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90141      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
90143      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
90961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
91001      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.81ms 
91002      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
91002      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.7ns 
91003      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93482      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
93483      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
94304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
94360      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.69ms 
94363      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
94363      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.91ns 
94364      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96868      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
96869      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
97659      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
97701      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.36ms 
97703      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
97703      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.7ns 
97704      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
100206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
101016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
101023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.58ms 
101025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
101025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.1ns 
101026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
103499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
104309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
104323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.46ms 
104324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
104324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.8ns 
104325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
106822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
107613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
107635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.85ms 
107638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
107640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.34ms 
107643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
110156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
110967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
110975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.62ms 
110978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
110978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.2ns 
110979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
113472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
114286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
114294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
114296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
114297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.31ns 
114298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
116797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
117589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
117596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.61ms 
117598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
117598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.8ns 
117599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
120092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
120907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
120911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
120912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
120912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89ns 
120913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
123384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
124193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
124204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ms 
124205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
124205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.1ns 
124206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
126703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
127489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
127543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.28ms 
127544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
127545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.2ns 
127545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
130040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
130851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
130869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.74ms 
130870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
130871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 
130871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
133356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
134167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
134186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.45ms 
134187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
134187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.7ns 
134188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
136681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
137468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
137486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.21ms 
137487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
137487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.6ns 
137488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
139980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
140791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
140808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.11ms 
140809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
140809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
140810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
143282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
144097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
144137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.14ms 
144138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
144138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
144139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
146639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
147425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
147428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
147430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
147430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.9ns 
147431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
149913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
150723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
150727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
150729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
150729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.5ns 
150730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
153195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
154003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
154012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
154013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
154013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.3ns 
154014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
156487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
157297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
157306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ms 
157309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
157309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.7ns 
157310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
159797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
160607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
160626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.01ms 
160627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
160627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.9ns 
160628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
163115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
163930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
163939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
163941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
163941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
163941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
166407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
167219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
167222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
167224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
167224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.3ns 
167225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
169729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
170536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
170540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
170541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
170541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
170542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
173013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
173829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
173833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
173835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
173836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.3ns 
173837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
176303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
177111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
177177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.47ms 
177179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
177179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.9ns 
177180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
179667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
180476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
180554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.52ms 
180556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
180556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
180556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
183023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
183833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
183836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
183838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
183838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
183839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
186302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
187108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
187143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.44ms 
187144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
187144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 213ns 
187145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
189630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
190437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
190466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.78ms 
190467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
190467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
190468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
192946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
193759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
193762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
193763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
193763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
193765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
196239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
197047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
197186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 127.91ms 
197188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
197189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.5ns 
197189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
199686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
200494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
200505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ms 
200506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
200506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
200507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
202981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
203790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
203798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.03ms 
203799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
203799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
203800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
206283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
207076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
207092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.41ms 
207093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
207093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
207094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
209576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
210384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
210399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.95ms 
210402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
210402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
210402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
212930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
213734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
213738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
213739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
213739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
213740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
216193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
217002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
217006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
217010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
217010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.8ns 
217011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
219499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
220312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
220334     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.66ms 
220339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
220339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.81ns 
220341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
222832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
223643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
223659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.32ms 
223660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
223660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
223661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
226125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
226936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
226951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.78ms 
226952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
226952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
226953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
229439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
230252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
230255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
230257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
230257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
230258     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.48s 
232734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
233541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
233545     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
233546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
233546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
233547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
236006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
236817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
236823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.78ms 
236825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
236825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
236826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
239307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
240117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
240120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
240121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
240121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
240122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
242587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
243393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
243395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 676.41ns 
243396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
243396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
243397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
245858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
246664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
246668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
246669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
246669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
246670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
249152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
249935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
249938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
249939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
249939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
249940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
252427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
253239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
253302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.91ms 
253304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
253305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
253306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
255785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
256593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
256632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.87ms 
256634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
256634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
256634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
259142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
259926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
259956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.14ms 
259958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
259959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.4ns 
259960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
262443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
263252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
263294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.05ms 
263295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
263295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85ns 
263296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
265760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
266572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
266601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.1ms 
266602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
266602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
266603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
269085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
269868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
269949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.96ms 
269950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
269951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.7ns 
269951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
272415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
273226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
273252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.05ms 
273253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
273254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
273254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
275718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
276524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
276544     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.41ms 
276546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
276546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
276546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
279025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
279814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
279876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.72ms 
279878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
279878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
279879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
282339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
283151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
283174     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.82ms 
283176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
283176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.9ns 
283177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
285645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
286451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
286480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.02ms 
286482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
286482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.2ns 
286483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
288970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
289781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
289815     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.31ms 
289817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
289817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.2ns 
289818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
292282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
293090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
293117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.79ms 
293118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
293118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
293119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
295576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
296382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
296408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.81ms 
296410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
296410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
296410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
298892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
299712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
299735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.94ms 
299736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
299736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
299737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
302199     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
303005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
303031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.27ms 
303032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
303032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
303033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
305491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
306297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
306322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.75ms 
306324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
306324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
306324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
308816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
309623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
309632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
309633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
309633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
309634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
312094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
312900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
312919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.35ms 
312921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
312921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
312921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
315376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
316182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
316186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
316187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
316188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
316188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
318668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
319480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
319482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 701.91ns 
319484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
319484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
319484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
321946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
322759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
322762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 798.41ns 
322764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
322764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
322765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
325220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
326029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
326036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.14ms 
326043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
326045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.05ms 
326046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
328535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
329319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
329326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
329327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
329327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
329328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
331818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
332631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
332645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.76ms 
332646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
332646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
332646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
335109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
335919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
335923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
335924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
335924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
335925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
338410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
339194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
339196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 573.82ns 
339198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
339198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
339198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
341678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
342485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
342491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.93ms 
342492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
342492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
342493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
344956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
345764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
345766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 705.32ns 
345768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
345768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
345768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
348245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
349029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
349031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 613.61ns 
349033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
349033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
349033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
351510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
352325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
352327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 632.21ns 
352329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
352330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.2ns 
352330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
354793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
355605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
355609     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
355611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
355611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
355611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
358092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
358880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
358889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.21ms 
358890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
358890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
358891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
361381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
362188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
362192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
362193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
362193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
362194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
364654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
365460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
365468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.35ms 
365469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
365469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
365470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
367952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
368735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
368740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
368741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
368741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
368742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
371218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
372026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
372043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.84ms 
372045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
372045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
372046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
374507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
375313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
375316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
375318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
375318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
375319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
377800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
378585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
378589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
378590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
378590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
378591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
381066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
381873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
381877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
381878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
381878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
381879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
384332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
385138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
385158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.09ms 
385159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
385159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
385160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
387638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
388443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
388447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 733.01ns 
388449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
388449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
388450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
390905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
391707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
391747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.6ms 
391749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
391749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
391749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
394231     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
395013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
395017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
395018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
395018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
395019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
397496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
398302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
398325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.62ms 
398327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
398328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.1ns 
398328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
400786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
401592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
401614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.76ms 
401615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
401615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
401616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
404102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
404906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
404931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.07ms 
404932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
404933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
404933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
407417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
408224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
408226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 564.91ns 
408227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
408228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
408228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
410707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
411512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
411518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
411519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
411519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
411520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
413987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
414796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
414800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
414802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
414802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.1ns 
414803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
417276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
418082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
418084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 869.31ns 
418086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
418086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
418086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
420548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
421355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
421358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 955.01ns 
421359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
421359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
421360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
423837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
424652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
424655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
424656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
424656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
424657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
427116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
427926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
427929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
427931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
427931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
427931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
430408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
431215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
431225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.39ms 
431226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
431227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
431227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
433700     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
434509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
434520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.74ms 
434522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
434522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
434523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
436998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
437809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
437822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.26ms 
437824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
437825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
437826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
440291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
441106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
441121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.44ms 
441122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
441123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
441123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
443598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
444412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
444416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
444418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
444418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
444418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
446904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
447695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
447701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ms 
447702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
447702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
447702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
450182     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
450998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
451000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 738.51ns 
451001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
451001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
451002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
453478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
454290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
454293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
454294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
454294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
454295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
456752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
457565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
457568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 839.81ns 
457570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
457570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.4ns 
457571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
460053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
460866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
460878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.47ms 
460879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
460879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
460880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
463355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
464147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
464151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
464153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
464153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
464154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
466629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
467443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
467450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.98ms 
467452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
467452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.6ns 
467453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
469930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
470745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
470747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 756.11ns 
470748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
470748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
470749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
473229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
474022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
474024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 652.01ns 
474025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
474025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
474026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
476503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
477318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
477321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
477323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
477323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
477323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
479795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
480620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
480623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
480624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
480624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
480625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
483099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
483911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
483914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
483916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
483916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
483916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
486374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
487186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
487189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
487190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
487190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.4ns 
487191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
489663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
490477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
490484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
490485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
490485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
490486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
492959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
493774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
493776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
493778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
493778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
493778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
496258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
497077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
497088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.81ms 
497089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
497089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
497090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
499548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
500359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
500361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 716.61ns 
500362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
500363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
500363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
502831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
503643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
503650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.63ms 
503651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
503652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
503652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
506130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
506946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
506949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
506951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
506951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
506952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
509434     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
510249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
510251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 784.21ns 
510252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
510252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
510253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
512723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
513543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
513548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
513550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
513550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
513550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
516011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
516826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
516829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
516830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
516830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
516831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
519299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
520112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
520115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
520117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
520117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
520117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
522589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
523403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
523407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
523408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
523408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
523409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
525886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
526700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
526710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
526711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
526711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
526712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
529187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
530002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
530016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.65ms 
530017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
530017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
530018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
532501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
533315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
533331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.63ms 
533332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
533332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
533333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
535806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
536621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
536632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.03ms 
536633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
536633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
536634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
539106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
539923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
539934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.15ms 
539935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
539935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
539936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
542416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
543232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
543258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.79ms 
543259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
543259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
543260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
545741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
546562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
546589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.9ms 
546590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
546590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
546591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
549075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
549896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
549921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.9ms 
549922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
549922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
549923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
552408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
553227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
553241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.53ms 
553242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
553243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
553243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
555722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
556539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
556570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.59ms 
556571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
556571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
556572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
559051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
559868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
559916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.4ms 
559918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
559918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
559919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
562399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
563215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
563253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.94ms 
563255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
563255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
563255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
565732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
566547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
566590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.03ms 
566591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
566591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
566592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
569067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
569884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
569928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.99ms 
569930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
569930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
569931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
572402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
573219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
573340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.35ms 
573341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
573341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
573342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
575829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
576650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
576658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.95ms 
576659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
576659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
576660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
579138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
579955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
579963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.91ms 
579964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
579964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
579965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
582443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
583259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
583264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.67ms 
583265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
583265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
583266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
585741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
586557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
586575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.41ms 
586577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
586577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
586577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
589069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
589887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
589899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.53ms 
589901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
589901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
589901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
592380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
593194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
593197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
593199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
593199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
593199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
595667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
596485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
596502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.76ms 
596503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
596504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
596504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
598971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
599787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
599804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.15ms 
599805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
599805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
599806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
602275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
603092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
603112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.7ms 
603113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
603113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
603114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
605605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
606427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
606430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
606432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
606432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
606432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
608900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
609714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
609718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
609719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
609720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.2ns 
609720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
612191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
613006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
613013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.21ms 
613014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
613014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
613015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
615489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
616303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
616309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.46ms 
616310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
616310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
616311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
618801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
619618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
619687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.08ms 
619689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
619689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
619690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
622163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
622979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
623006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.15ms 
623007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
623007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
623008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
625480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
626298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
626320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.73ms 
626322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
626322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
626322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
628813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
629627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
629629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 288.7ns 
629631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
629631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
629632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
632108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
632924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
633127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 191.44ms 
633130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
633130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.3ns 
633131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
635612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
636432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
636483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46ms 
636485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
636485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
636485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
638981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
639799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
639801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 336.5ns 
639803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
639803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
639805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
642279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
643096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
643098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 362.9ns 
643099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
643099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
643100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
645591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
646404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
646406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 406.21ns 
646407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
646407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
646408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
648876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
649690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
649692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 555.91ns 
649693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
649693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
649694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
652162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
653006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
653107     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
653124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 115.74ms 
653130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
653131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.6ns 
653132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
655617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
655617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
656431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
656479     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
656480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.52ms 
656481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
656482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
656483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
658973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
658973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
659833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
659835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 
659864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
659906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
659926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
659932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
659940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
659943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
659944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
659948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
659952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
659955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
659959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
659960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
660163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
660164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
660165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
660167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
660168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
660283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
660285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
660286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
660287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
660289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
660290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
660436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
660438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
660439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
660440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
660441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
660443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
660555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
660556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
660557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
660558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
660559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
660560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
660566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
660567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
660567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
660569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
660570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
660571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
660577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
660578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
660579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
660582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
660583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
660583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
660745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
660745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
660747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
660868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
660870     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)'' 
660873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
660874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
660875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
660876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
660877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
660879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
660882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
660883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
660884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
660885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
660886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
661006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
661009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
661010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
661011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
661013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
661014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
661016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
661127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
661131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
661132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
661134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
661135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
661135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
661137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
661138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
661227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
661228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
661308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
661312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
661317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
661318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
661320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
661322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
661323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
661323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
661323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
661325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
661332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
661336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
661427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
661428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
661430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
661432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
661432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
661432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
661433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
661434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
661487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
661491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
661583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
661584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
661586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
661587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
661588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
661589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
661729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
661733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
661736     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)'' 
661738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
661739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
661740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
661741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
661741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
661750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
661752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
661756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
661757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
661850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
661851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
661852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
661853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
661853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
661854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
661952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
661954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
661955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
661956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
661957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
661958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
661958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
661959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
662042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
662044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
662118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
662119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
662120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
662124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
662127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
662132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
662260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
662261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
662262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
662263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
662274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
662402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
665607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
665608     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)'' 
665613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
665613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
665614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
665615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
665615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
665622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
665624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
665625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
665625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
665626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
665711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
665715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
665716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
665716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
665717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
665717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
665718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
665849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
665850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
665851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
665852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
665853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
665853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
665854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
665855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
665924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
665925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
665991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
665995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
665998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
665999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
666000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
666000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
666009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
666082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
666083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
666083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
666084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
666149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
666157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
666158     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)'' 
666160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
666160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
666161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
666162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
666162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
666172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
666173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
666174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
666174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
666175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
666254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
666256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
666257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
666257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
666258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
666341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
666345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
666346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
666347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
666347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
666348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
666349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
666439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
666440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
666441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
666442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
666443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
666443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
666444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
666445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
666446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
666446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
666447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
666448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
666448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
666448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
666449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
666529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
666530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
666536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
666606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
666679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
666680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
666681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
666682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
666683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
666683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
666683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
666684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
666685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
666762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
666768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
666849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
666850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
666851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
666852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
666852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
666853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
666853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
666854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
666858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
666859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
666931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
666936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
666941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
667033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
667034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
667034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
667035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
667036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
667036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
667036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
667037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
667087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
667088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
667089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
667089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
667090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
667095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
667100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
667219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
667354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
667355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
667356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
667357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
667512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
667593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
667593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
670385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
670390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
670391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
670391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
670392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
670499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
670500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
670501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
670502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
670502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
670601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
673345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
676262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
676267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
676269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
676269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
676270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
676376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
676377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
676378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
676379     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)' ...' 
676380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
677399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
677399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
677400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
680086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
680923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
680924     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
680924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
680933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
680943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
680946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
680947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
680948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
680952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
680954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
680957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
680959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
680960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
680969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
680971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
680971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
681015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
681016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
681017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
681017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
681018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
681083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
681084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
681085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
681086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
681086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
681090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
681090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
681090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
681092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
681092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
681093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
681170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
681171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
681171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
681173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
681174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
681174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
681258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
681259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
681260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
681260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
681261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
681262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
681263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
681263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
681264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
681265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
681265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
681266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
681266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
681267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
681267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
681268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
681268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
681270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
681271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
681273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
681311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
681313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
681364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
681365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
681367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
681368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
681369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
681369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
681413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
681416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
681417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
681419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
681420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
681421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
681421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
681467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
681469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
681472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
681522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
681571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
681571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.7ns 
681572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
684163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
684163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
685022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
685054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.52ms