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

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

tests
0

failures
0

ignored
11m15.38s

duration
100%

successful

Tests

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

Standard output

588        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
615        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.49ms 
822        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
836        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)

1770       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1774       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1778       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1779       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3250       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8743       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.92s 
8805       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8839       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.2ns 
8853       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8855       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.83ms 
8859       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11894      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
11896      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12937      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12970      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.35ms 
12986      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12988      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.72ms 
12990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15862      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
15862      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16814      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.32ms 
16817      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16818      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 603.51ns 
16819      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19472      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
19473      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20404      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.44ms 
20410      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20410      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.91ns 
20412      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23055      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
23055      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23925      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23931      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
23935      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23936      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 877.71ns 
23937      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26505      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
26505      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
27344      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
27383      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.94ms 
27386      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
27386      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.81ns 
27388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
29978      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30837      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30866      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.49ms 
30872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30873      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.4ns 
30873      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33465      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
33465      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
34305      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
34309      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 795.21ns 
34312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
34312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.31ns 
34313      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36866      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
36866      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37713      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37717      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 653.71ns 
37720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341ns 
37721      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40255      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
40256      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
41088      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
41091      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 681.71ns 
41094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
41094      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.21ns 
41095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43621      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
43622      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
44454      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
44457      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 678.81ns 
44460      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
44460      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.5ns 
44461      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47002      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
47003      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
47816      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
47820      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.91ns 
47827      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
47828      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.21ns 
47829      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50547      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
50547      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
51357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
51396      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.15ms 
51402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
51402      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 502.91ns 
51404      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
53977      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
54777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
54815      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.61ms 
54822      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
54822      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326ns 
54823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57360      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
57361      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
58164      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
58282      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.74ms 
58286      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
58286      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 418.91ns 
58287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60814      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
60815      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
61609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
61615      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.74ms 
61617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
61618      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.4ns 
61619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64143      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
64144      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
64938      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
64942      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
64946      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
64946      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.11ns 
64948      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67473      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
67474      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
68275      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
68315      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.96ms 
68321      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
68321      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.9ns 
68322      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70903      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
70904      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
71721      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
71734      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.61ms 
71737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
71737      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.71ns 
71738      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74223      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
74223      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
75052      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
75071      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.92ms 
75075      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
75075      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.5ns 
75081      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77607      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
77607      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
78429      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
78445      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.55ms 
78449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
78449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.4ns 
78450      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80962      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
80962      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
81795      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
81808      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.76ms 
81811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
81812      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.2ns 
81813      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84329      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
84329      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
85156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
85174      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.8ms 
85176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
85176      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.2ns 
85177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87674      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
87674      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
88532      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
88537      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
88548      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
88548      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.11ns 
88550      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91033      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
91034      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
91865      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
91910      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.38ms 
91914      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
91914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 395.02ns 
91915      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94401      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
94401      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
95224      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
95296      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.33ms 
95301      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
95301      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.82ns 
95302      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97783      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
97783      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
98598      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
98629      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26ms 
98631      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
98631      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.72ns 
98632      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
101123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
101939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
101951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.75ms 
101952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
101953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.6ns 
101953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
104433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
105249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
105262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.07ms 
105266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
105267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.06ms 
105269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
107791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
108613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
108624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.84ms 
108625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
108625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.5ns 
108626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
111105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
111922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
111929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
111931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
111932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.4ns 
111933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
114412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
115226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
115233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 
115236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
115236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.22ns 
115237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
117710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
118522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
118528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
118529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
118530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.5ns 
118530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
121020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
121805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
121809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
121810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
121810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.91ns 
121811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
124328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
125115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
125124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
125126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
125126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.91ns 
125127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
127631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
128414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
128449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.49ms 
128453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
128467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 13.96ms 
128468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
131040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
131846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
131866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.76ms 
131867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
131867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.01ns 
131869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
134365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
135151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
135166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.04ms 
135167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
135168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.11ns 
135168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
137657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
138446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
138461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.31ms 
138464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
138464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.12ns 
138465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
140940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
141763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
141783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.38ms 
141791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
141792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.22ns 
141793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
144298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
145107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
145138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.26ms 
145141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
145142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.42ns 
145143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
147614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
148421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
148424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
148426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
148426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.31ns 
148426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
150891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
151715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
151718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
151720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
151720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
151721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
154188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
155005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
155012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
155014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
155014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.91ns 
155015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
157480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
158298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
158311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.69ms 
158314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
158314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296.02ns 
158315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
160777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
161586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
161602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.15ms 
161604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
161604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.91ns 
161605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
164068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
164881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
164889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
164890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
164890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
164891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
167352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
168166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
168169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
168171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
168171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.91ns 
168172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
170671     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
171481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
171485     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
171487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
171487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.51ns 
171487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
173982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
174792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
174796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
174799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
174799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 631.73ns 
174800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
177263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
178075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
178143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.74ms 
178149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
178150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.22ns 
178151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
180627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
181437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
181503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.7ms 
181506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
181507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 356.22ns 
181508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
184003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
184813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
184816     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
184818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
184818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.11ns 
184819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
187282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
188092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
188122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.1ms 
188124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
188124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.01ns 
188125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
190585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
191395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
191416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.65ms 
191417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
191417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.41ns 
191418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
193880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
194664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
194667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
194668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
194668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
194669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
197156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
197943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
198054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.85ms 
198058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
198058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.61ns 
198059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
200580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
201391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
201399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.42ms 
201401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
201401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
201402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
203893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
204678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
204684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms 
204685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
204685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
204686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
207212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
207998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
208013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.13ms 
208014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
208014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.11ns 
208015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
210514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
211295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
211306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
211309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
211309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
211309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
213792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
214580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
214584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
214585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
214585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.41ns 
214586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
217044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
217857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
217861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
217863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
217863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.21ns 
217864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
220330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
221141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
221156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.92ms 
221158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
221158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
221159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
223633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
224451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
224473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.48ms 
224477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
224477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 780.44ns 
224479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
226954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
227765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
227777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.28ms 
227780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
227780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.01ns 
227781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
230257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
231085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
231089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 994.65ns 
231091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
231091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.91ns 
231092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
233582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
234388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
234391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
234392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
234392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.7ns 
234393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
236854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
237661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
237666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
237667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
237667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
237668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
240121     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
240926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
240928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 871.14ns 
240930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
240930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
240930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
243382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
244195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
244197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 536.22ns 
244198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
244199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
244199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
246656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
247461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
247465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
247467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
247467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
247468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
249922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
250728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
250730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 712.62ns 
250732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
250732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
250732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
253200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
254007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
254043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.39ms 
254045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
254046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.41ns 
254047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
256507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
257318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
257354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.65ms 
257357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
257357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.41ns 
257358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
259835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
260645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
260666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.96ms 
260668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
260669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.51ns 
260670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
263155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
263936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
263997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.97ms 
263999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
263999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
264000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
266449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
267230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
267248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.89ms 
267249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
267250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.31ns 
267250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
269738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
270519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
270553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.3ms 
270555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
270555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.21ns 
270556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
273045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
273827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
273845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.48ms 
273846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
273846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
273847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
276351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
277138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
277152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.02ms 
277153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
277153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
277154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279642     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
279642     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
280429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
280445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.42ms 
280447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
280447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
280448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
282987     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
283769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
283782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.45ms 
283784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
283784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
283785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
286249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
287058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
287076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.41ms 
287077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
287077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
287078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
289535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
290337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
290354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.49ms 
290355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
290355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
290356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
292808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
293616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
293642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.83ms 
293644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
293644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
293646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
296101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
296905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
296921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
296923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
296923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 
296924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
299371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
300181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
300196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.44ms 
300198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
300198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
300199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
302654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
303459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
303476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.44ms 
303478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
303478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.5ns 
303479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
305932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
306747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
306762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.67ms 
306764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
306764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
306764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
309223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
310031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
310037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
310039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
310039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
310040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
312497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
313303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
313314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.81ms 
313316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
313316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
313316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
315773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
316580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
316584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
316586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
316586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.81ns 
316587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
319042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
319873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
319878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 644.92ns 
319880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
319880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
319881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
322332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
323152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
323154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 735.02ns 
323156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
323156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
323157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
325603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
326411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
326422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.17ms 
326428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
326428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 351.91ns 
326429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
328888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
329699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
329704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
329706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
329706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
329707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
332161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
332967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
332977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ms 
332979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
332979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
332979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
335437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
336249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
336253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
336254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
336254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
336255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
338695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
339477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
339480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 486.12ns 
339481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
339481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
339482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
341946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
342727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
342732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
342733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
342733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
342734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
345201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
345983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
345985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 544.72ns 
345987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
345987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
345987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
348452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
349239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
349241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 545.81ns 
349243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
349243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
349243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
351725     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
352507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
352509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 560.22ns 
352510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
352510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
352511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
354974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
355759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
355763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
355764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
355765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
355765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
358209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
359012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
359020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.12ms 
359021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
359021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
359022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
361467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
362273     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
362277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
362278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
362278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
362279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
364743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
365572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
365578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
365579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
365579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
365580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
368033     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
368839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
368844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
368846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
368846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.31ns 
368847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
371296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
372118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
372134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.34ms 
372139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
372139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.81ns 
372140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
374586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
375394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
375397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
375399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
375399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
375400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
377862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
378674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
378678     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
378679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
378679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
378680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
381152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
381963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
381967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
381968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
381968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
381969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
384423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
385232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
385245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.25ms 
385246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
385246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
385247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
387719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
388531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
388536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 446.21ns 
388540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
388540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.8ns 
388541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
391011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
391817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
391843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.59ms 
391844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
391845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
391845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
394329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
395142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
395145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
395147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
395147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
395147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
397626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
398434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
398449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.03ms 
398450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
398450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
398451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
400900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
401708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
401724     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.45ms 
401727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
401727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.31ns 
401728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
404197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
404978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
404995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.33ms 
404997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
404997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
404998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
407469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
408257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
408260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 525.92ns 
408264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
408264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.81ns 
408265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
410744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
411528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
411534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.37ms 
411535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
411535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
411536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
414007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
414792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
414795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
414796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
414796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
414797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
417262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
418048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
418051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 802.32ns 
418052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
418052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
418053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
420517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
421303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
421305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 754.32ns 
421307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
421307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
421307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
423748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
424567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
424570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
424572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
424572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
424572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
427017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
427825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
427828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 994.93ns 
427829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
427829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
427830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
430268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
431078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
431087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.78ms 
431088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
431088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
431089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
433538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
434348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
434355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
434356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
434357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
434357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
436799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
437619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
437625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
437627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
437628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.6ns 
437628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
440095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
440917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
440925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.44ms 
440926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
440926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
440927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
443363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
444182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
444186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
444188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
444189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.13ms 
444190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
446626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
447448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
447452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
447454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
447454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
447454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
449893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
450709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
450712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 721.72ns 
450713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
450713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
450714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
453151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
453991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
453995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
453999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
453999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.51ns 
454000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
456444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
457262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
457265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
457266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
457266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
457267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
459698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
460513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
460522     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.36ms 
460523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
460523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
460524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
462974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
463796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
463800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
463804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
463804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.61ns 
463806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
466244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
467063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
467068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
467069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
467069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
467070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
469503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
470318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
470320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 794.02ns 
470323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
470323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215ns 
470324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
472763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
473580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
473582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.92ns 
473583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
473583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
473584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
476042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
476859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
476862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
476863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
476863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
476864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
479303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
480118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
480121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 844.12ns 
480122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
480122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
480123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
482562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
483382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
483385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
483386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
483386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
483387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
485862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
486656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
486659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 931.62ns 
486660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
486660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
486661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
489120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
489914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
489917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
489919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
489919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
489919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
492382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
493177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
493179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 784.22ns 
493181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
493181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
493182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
495669     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
496490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
496498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.38ms 
496500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
496500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
496500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
498949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
499769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
499771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.62ns 
499772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
499772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
499773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
502215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
503032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
503038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
503039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
503039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
503040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
505473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
506288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
506291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 898.32ns 
506293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
506293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.51ns 
506294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
508731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
509550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
509552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 675.42ns 
509553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
509553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
509554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
512015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
512828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
512831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
512833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
512833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
512833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
515298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
516092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
516095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 895.72ns 
516096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
516096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
516097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
518588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
519415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
519419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
519421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
519422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.11ns 
519422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
521867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
522683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
522685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
522687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
522687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
522687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
525127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
525948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
525955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
525957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
525957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
525958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
528401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
529219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
529227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.43ms 
529228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
529228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
529229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
531687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
532482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
532490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
532492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
532492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
532492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
534965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
535759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
535765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ms 
535766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
535766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
535767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
538239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
539058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
539064     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.12ms 
539065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
539065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
539066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
541505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
542377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
542387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.08ms 
542389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
542389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
542390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
544853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
545669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
545679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.46ms 
545680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
545680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
545681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
548140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
548933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
548942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.02ms 
548944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
548944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
548944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
551401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
552218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
552225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.1ms 
552227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
552227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
552228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
554686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
555505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
555524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.99ms 
555525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
555525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
555526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
557964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
558787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
558807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.17ms 
558809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
558809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
558810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
561285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
562103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
562121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.2ms 
562122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
562122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
562123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
564578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
565414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
565432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.59ms 
565433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
565433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
565434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
567902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
568736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
568754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.52ms 
568756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
568756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
568757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
571238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
572034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
572114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.9ms 
572116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
572116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
572117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
574565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
575385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
575390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
575391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
575391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
575392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
577833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
578669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
578673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 
578675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
578675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
578676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
581139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
581960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
581967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.38ms 
581969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
581970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.71ns 
581970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
584407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
585236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
585249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
585252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
585252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
585253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
587687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
588505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
588512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
588513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
588513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
588514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
590968     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
591787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
591790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
591791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
591791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
591792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
594227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
595046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
595056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ms 
595057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
595057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
595058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
597518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
598314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
598324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.81ms 
598326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
598326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
598327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
600813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
601632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
601645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.21ms 
601647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
601647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.6ns 
601647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
604100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
604925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
604928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 891.12ns 
604929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
604929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
604930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
607391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
608211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
608214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
608216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
608216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
608216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
610673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
611494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
611500     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ms 
611501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
611502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
611502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
613984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
614806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
614810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
614812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
614812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
614813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
617270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
618092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
618131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.71ms 
618132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
618132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
618133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
620597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
621392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
621410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.36ms 
621411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
621411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
621412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
623878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
624696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
624710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.38ms 
624713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
624713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.9ns 
624714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
627184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
627983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
627985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 252.81ns 
627987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
627987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
627988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
630469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
631289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
631366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.2ms 
631368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
631368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
631369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
633837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
634665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
634698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.82ms 
634700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
634700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.4ns 
634701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
637194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
638014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
638016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 278.71ns 
638018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
638018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
638018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
640490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
641310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
641312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 214.41ns 
641314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
641314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
641314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
643779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
644599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
644601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 217.4ns 
644602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
644602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
644603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
647075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
647893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
647895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 330.21ns 
647896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
647896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
647897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
650335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
651154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
651241     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
651249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.94ms 
651252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
651252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.21ns 
651253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
653739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
654560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
654610     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
654610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.39ms 
654612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
654612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
654613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
657128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
657928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
657930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4ns 
657957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
658004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
658024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
658035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
658044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
658045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
658047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
658047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
658051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
658052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
658054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
658056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
658281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
658282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
658284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
658285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
658287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
658422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
658423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
658427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
658428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
658430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
658431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
658617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
658618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
658619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
658620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
658621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
658622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
658732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
658733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
658734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
658735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
658735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
658736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
658742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
658743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
658744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
658745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
658746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
658747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
658753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
658754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
658755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
658755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
658756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
658757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
658881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
658882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
658883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
659003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
659004     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)'' 
659005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
659007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
659008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
659009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
659009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
659010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
659013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
659014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
659015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
659016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
659017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
659124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
659127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
659128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
659129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
659130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
659130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
659131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
659254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
659255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
659256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
659257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
659258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
659258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
659259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
659259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
659361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
659362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
659457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
659462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
659467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
659468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
659469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
659470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
659470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
659471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
659472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
659472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
659480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
659485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
659584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
659585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
659586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
659587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
659588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
659588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
659589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
659590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
659642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
659649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
659757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
659759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
659760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
659761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
659763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
659764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
659915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
659919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
659920     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)'' 
659921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
659922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
659923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
659924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
659924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
659934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
659934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
659935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
659938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
660030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
660032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
660033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
660034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
660034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
660035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
660136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
660137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
660139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
660140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
660141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
660142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
660142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
660143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
660256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
660258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
660336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
660337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
660338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
660343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
660347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
660351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
660473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
660474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
660475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
660476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
660487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
660579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
664161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
664162     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)'' 
664166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
664168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
664169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
664169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
664170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
664178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
664179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
664180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
664181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
664182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
664276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
664280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
664281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
664282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
664283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
664283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
664284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
664380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
664382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
664383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
664384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
664385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
664385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
664386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
664387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
664466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
664468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
664550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
664555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
664559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
664560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
664561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
664562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
664573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
664661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
664663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
664664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
664665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
664740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
664750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
664751     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)'' 
664753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
664754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
664755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
664756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
664757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
664768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
664769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
664771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
664772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
664773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
664866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
664867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
664868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
664869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
664871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
664965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
664970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
664971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
664972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
664973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
664974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
664975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
665076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
665078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
665079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
665080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
665081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
665082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
665082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
665083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
665084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
665085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
665086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
665087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
665087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
665088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
665088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
665176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
665178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
665184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
665263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
665345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
665346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
665347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
665348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
665349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
665350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
665351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
665351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
665352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
665438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
665445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
665536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
665538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
665539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
665540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
665540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
665541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
665541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
665542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
665547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
665548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
665630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
665635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
665641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
665742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
665744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
665745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
665746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
665747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
665747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
665748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
665748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
665804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
665806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
665807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
665808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
665808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
665817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
665822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
665987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
666075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
666077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
666078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
666079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
666247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
666335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
666336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
669264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
669269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
669270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
669271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
669272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
669387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
669388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
669390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
669391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
669392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
669497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
672428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
675512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
675517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
675518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
675519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
675520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
675633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
675634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
675635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
675636     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)' ...' 
675637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
676781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
676781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.4ns 
676782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
679336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
680188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
680190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.1ns 
680190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
680199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
680208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
680211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
680213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
680215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
680220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
680220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
680225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
680225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
680228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
680238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
680238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
680240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
680292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
680292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
680293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
680294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
680294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
680363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
680364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
680364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
680365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
680366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
680370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
680371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
680371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
680371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
680372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
680373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
680458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
680458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
680459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
680459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
680461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
680461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
680545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
680546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
680547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
680547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
680548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
680548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
680549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
680549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
680550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
680550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
680550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
680551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
680551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
680551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
680552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
680552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
680553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
680553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
680554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
680556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
680592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
680593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
680647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
680648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
680649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
680650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
680651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
680652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
680699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
680701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
680702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
680703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
680704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
680705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
680705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
680746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
680748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
680751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
680801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
680853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
680853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
680853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
683389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
684242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
684258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.79ms