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

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

tests
0

failures
0

ignored
11m12.70s

duration
100%

successful

Tests

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

Standard output

577        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
599        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.26ms 
811        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
825        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)

1703       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1705       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1707       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1708       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3074       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8660       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.85s 
8736       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8773       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.4ns 
8789       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8789       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.81ns 
8794       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11835      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
11838      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12812      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12843      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.5ms 
12854      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12854      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.2ns 
12857      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15565      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
15566      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16460      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16474      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.07ms 
16478      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16479      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.91ns 
16481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19130      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.65s 
19131      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
20011      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
20018      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.37ms 
20022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
20023      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 831.41ns 
20024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22617      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
22618      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23455      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23461      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
23465      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23465      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 511.31ns 
23466      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25999      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
26000      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26890      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.52ms 
26893      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26894      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.23ms 
26897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29486      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
29486      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30291      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30312      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.4ms 
30326      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30326      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 516.01ns 
30328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32871      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
32871      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33706      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33710      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 830.71ns 
33713      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33713      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.71ns 
33714      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36218      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
36218      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37048      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 659.71ns 
37051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37051      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.4ns 
37052      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39548      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
39549      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
40382      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
40385      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 648.91ns 
40391      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
40391      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349ns 
40393      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42870      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
42871      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43697      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 649.11ns 
43700      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43700      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.01ns 
43701      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46235      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
46236      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
47043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
47048      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
47053      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
47053      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.11ns 
47055      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49628      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
49628      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
50422      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
50519      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 89.65ms 
50526      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
50526      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 521.71ns 
50527      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53051      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
53052      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53869      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
53945      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.35ms 
53949      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
53949      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 704.81ns 
53952      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56432      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
56433      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
57245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
57401      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 147.46ms 
57405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
57405      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.5ns 
57406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59890      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
59891      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
60704      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
60710      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
60711      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
60711      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.5ns 
60712      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63174      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
63175      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
64017      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
64022      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
64024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
64024      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.71ns 
64026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66527      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
66527      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
67313      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
67352      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.45ms 
67353      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
67354      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.2ns 
67355      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69847      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
69847      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
70659      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
70675      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.7ms 
70677      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
70677      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.2ns 
70678      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73131      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
73131      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
73955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
73974      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
73977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
73977      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.2ns 
73981      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76451      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
76452      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
77261      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
77276      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.91ms 
77278      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
77278      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.7ns 
77279      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79742      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
79742      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
80561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
80576      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.16ms 
80577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
80577      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112ns 
80578      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83057      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
83057      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
83841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
83865      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.64ms 
83867      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
83867      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122ns 
83868      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86341      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
86341      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
87123      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
87126      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
87128      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
87128      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.4ns 
87129      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89606      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
89606      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
90420      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
90477      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.89ms 
90480      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
90480      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 355.71ns 
90482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92973      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
92974      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
93788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
93844      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.01ms 
93845      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
93846      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.4ns 
93847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96299      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
96299      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
97112      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
97154      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.06ms 
97156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
97156      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.7ns 
97157      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99632      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
99633      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
100416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
100424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
100425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
100425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.7ns 
100426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
102904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
103690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
103703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.46ms 
103705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
103705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.2ns 
103706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
106190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
107007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
107021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.3ms 
107024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
107024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 329.11ns 
107025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
109482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
110290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
110297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.31ms 
110299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
110299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
110300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
112762     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
113568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
113575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.37ms 
113577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
113577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
113578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
116039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
116845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
116852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
116854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
116854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.4ns 
116855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
119341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
120123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
120127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
120129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
120129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172ns 
120130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
122600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
123380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
123421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.77ms 
123422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
123422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.4ns 
123423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
125876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
126680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
126727     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.57ms 
126729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
126729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
126730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
129206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
130013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
130030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.14ms 
130035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
130036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.7ns 
130037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
132482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
133290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
133307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.43ms 
133308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
133308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.6ns 
133309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
135781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
136562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
136579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.25ms 
136580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
136581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.1ns 
136581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
139055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
139843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
139858     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.75ms 
139860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
139860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.3ns 
139861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
142332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
143138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
143175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.55ms 
143176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
143176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.4ns 
143177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
145623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
146425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
146429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
146430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
146430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
146431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
148873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
149685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
149689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
149691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
149692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 280.2ns 
149693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
152152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
152955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
152963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
152964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
152964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
152965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
155429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
156211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
156218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
156220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
156220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
156221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
158685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
159491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
159510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.28ms 
159512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
159512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.9ns 
159513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
161964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
162770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
162777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.63ms 
162779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
162779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
162780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
165250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
166060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
166063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
166066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
166066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277ns 
166067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
168517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
169319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
169324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
169326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
169326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259ns 
169327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
171791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
172570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
172574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
172577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
172577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.6ns 
172578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
175037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
175816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
175907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.34ms 
175912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
175912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 854.51ns 
175914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
178386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
179196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
179266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.01ms 
179268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
179268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.6ns 
179269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
181715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
182524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
182529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
182531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
182531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.2ns 
182532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
184980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
185786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
185819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.31ms 
185821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
185822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.1ns 
185823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
188262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
189084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
189111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.84ms 
189112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
189112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
189113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
191578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
192356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
192360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
192363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
192364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.21ns 
192365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
194826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
195627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
195765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 127.88ms 
195768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
195768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.4ns 
195769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
198222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
199030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
199040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.62ms 
199042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
199042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
199043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
201486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
202297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
202304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.51ms 
202306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
202306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
202307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
204743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
205545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
205561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.94ms 
205563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
205563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
205564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
208038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
208818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
208830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
208832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
208832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
208833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
211291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
212092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
212096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
212097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
212097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
212098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
214548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
215353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
215357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ms 
215359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
215359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.3ns 
215360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
217807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
218612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
218633     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.04ms 
218634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
218634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
218635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
221073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
221878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
221893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.48ms 
221895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
221895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
221895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
224361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
225140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
225155     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.49ms 
225157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
225157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 
225158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
227629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
228407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
228411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
228412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
228413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
228413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
230878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
231681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
231686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
231687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
231687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
231688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
234130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
234933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
234938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
234939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
234939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
234940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
237383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
238189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
238194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
238195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
238197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.08ms 
238197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
240646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
241451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
241453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.31ns 
241455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
241455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
241456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
243937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
244718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
244722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
244723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
244724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
244724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
247200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
248005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
248008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 953.52ns 
248009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
248009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.4ns 
248010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
250459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
251260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
251310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.23ms 
251313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
251313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.2ns 
251314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
253765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
254569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
254607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.78ms 
254609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
254609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
254610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
257048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
257860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
257891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.93ms 
257892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
257893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
257893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
260367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
261147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
261190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.02ms 
261192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
261192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.5ns 
261193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
263658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
264435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
264467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.49ms 
264469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
264469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
264469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
266942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
267747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
267797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.6ms 
267800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
267800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.8ns 
267801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
270253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
271057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
271082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.36ms 
271084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
271084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
271085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
273529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
274331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
274350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.98ms 
274352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
274352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
274353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
276816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
277600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
277623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.88ms 
277626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
277626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.1ns 
277627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
280110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
280902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
280921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.36ms 
280922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
280922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.9ns 
280923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
283391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
284197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
284223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.49ms 
284224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
284224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.6ns 
284225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
286672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
287485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
287508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.04ms 
287510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
287510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns 
287511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
289962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
290771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
290797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.34ms 
290799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
290799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.5ns 
290800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
293251     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
294052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
294074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.73ms 
294076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
294076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
294077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
296545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
297323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
297342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.58ms 
297344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
297344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
297345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
299811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
300614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
300639     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.84ms 
300641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
300641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92ns 
300641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
303093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
303896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
303920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.7ms 
303923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
303923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.9ns 
303924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
306369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
307177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
307184     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.6ms 
307186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
307186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
307187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
309631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
310435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
310452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.11ms 
310453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
310453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
310454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
312916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
313697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
313701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
313703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
313703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
313704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
316172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
316952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
316994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.3ms 
316995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
316995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
316996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
319433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
320240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
320242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 772.01ns 
320244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
320244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
320244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
322696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
323507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
323514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
323515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
323515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
323516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
325958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
326763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
326769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.35ms 
326770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
326770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
326771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
329207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
330027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
330039     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.86ms 
330042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
330042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.3ns 
330043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
332518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
333300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
333304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
333305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
333305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
333306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
335776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
336582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
336584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.91ns 
336586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
336586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
336586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
339036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
339843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
339848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
339850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
339850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
339850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
342297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
343102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
343104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.91ns 
343106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
343106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
343106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
345555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
346361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
346363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 604.81ns 
346365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
346365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
346365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
348837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
349618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
349621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 643.51ns 
349622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
349622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
349623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
352091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
352878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
352884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
352885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
352886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
352886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
355348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
356159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
356168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.68ms 
356170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
356170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
356170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
358605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
359409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
359413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
359414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
359414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
359415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
361853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
362660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
362667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.14ms 
362669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
362669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
362669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
365112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
365918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
365923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
365924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
365924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
365926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
368401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
369196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
369212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.49ms 
369214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
369214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
369214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
371683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
372491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
372494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
372496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
372496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
372497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
374950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
375757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
375761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
375762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
375762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
375763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
378215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
379028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
379032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
379033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
379033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
379034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
381466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
382271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
382288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.73ms 
382289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
382289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
382290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
384751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
385530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
385535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 516.81ns 
385536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
385537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
385537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
387984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
388765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
388803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.87ms 
388805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
388805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.3ns 
388806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
391255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
392062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
392066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
392067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
392067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
392068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
394499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
395304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
395324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.74ms 
395326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
395326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
395327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
397759     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
398563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
398582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.78ms 
398583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
398584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
398584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
401043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
401823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
401846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.72ms 
401847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
401847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
401848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
404308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
405092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
405095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.41ns 
405098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
405098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
405098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
407547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
408352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
408357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.7ms 
408358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
408358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
408359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
410794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
411605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
411608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
411609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
411609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
411610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
414036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
414847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
414849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 897.61ns 
414851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
414851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
414851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
417302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
418087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
418089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 906.01ns 
418092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
418092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
418093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
420540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
421350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
421354     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
421356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
421356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204ns 
421357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
423795     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
424608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
424611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
424612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
424612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
424613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
427041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
427852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
427861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.78ms 
427863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
427863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
427864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
430325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
431137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
431148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.03ms 
431150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
431150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
431150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
433583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
434390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
434400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ms 
434402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
434402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
434403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
436835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
437652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
437664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.43ms 
437665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
437665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
437666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
440116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
440912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
440917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
440918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
440918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
440919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
443383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
444198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
444204     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
444206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
444206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
444206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
446643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
447460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
447463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 899.01ns 
447464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
447464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
447465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
449935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
450727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
450730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
450731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
450731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
450732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
453214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
454029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
454032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
454033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
454033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
454034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
456469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
457284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
457295     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ms 
457296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
457296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
457297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
459753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
460570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
460574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.48ms 
460576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
460576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
460577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
463021     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
463838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
463844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
463846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
463846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
463847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
466297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
467089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
467092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 762.91ns 
467093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
467093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
467094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469559     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
469559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
470375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
470377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 701.41ns 
470378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
470378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
470379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
472809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
473626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
473630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
473632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
473632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
473632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
476089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
476904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
476907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
476908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
476908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
476909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
479359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
480175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
480178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
480179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
480180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
480180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
482649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
483465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
483468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
483470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
483470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.6ns 
483470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
485917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
486735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
486740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
486741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
486742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
486742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
489198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
489991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
489994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
489995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
489995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
489996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
492454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
493272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
493283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.35ms 
493284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
493284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.2ns 
493285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
495738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
496528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
496530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 643.61ns 
496531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
496531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
496532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
498983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
499799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
499806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.99ms 
499807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
499807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
499808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
502264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
503057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
503060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 906.51ns 
503061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
503061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
503061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
505522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
506338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
506340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 783.51ns 
506341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
506341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
506342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
508802     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
509595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
509600     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
509602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
509602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
509602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
512073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
512887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
512890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
512892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
512892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
512892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
515357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
516173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
516178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
516180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
516180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218.2ns 
516181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
518615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
519428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
519432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
519435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
519435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
519436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
521890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
522702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
522707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.06ms 
522710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
522710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
522711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
525144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
525961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
525975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.72ms 
525976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
525976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.4ns 
525977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
528444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
529259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
529274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ms 
529275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
529275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
529276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
531735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
532549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
532559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.07ms 
532561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
532561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
532561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
535005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
535822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
535832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.27ms 
535833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
535833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
535834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
538292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
539107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
539131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.68ms 
539132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
539132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
539133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
541597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
542392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
542446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.3ms 
542447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
542447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.8ns 
542448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
544885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
545701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
545723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.86ms 
545724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
545724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
545725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
548181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
548994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
549008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.35ms 
549009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
549009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
549010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
551466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
552282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
552310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.49ms 
552311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
552311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
552312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
554754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
555570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
555614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.75ms 
555615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
555615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
555616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
558078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
558894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
558929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.16ms 
558931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
558931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
558932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
561384     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
562200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
562239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.72ms 
562241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
562241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
562241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
564698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
565517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
565559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.1ms 
565560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
565560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
565561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
568000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
568817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
568928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 104ms 
568930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
568930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
568931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
571391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
572210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
572222     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.26ms 
572223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
572223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
572224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
574683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
575501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
575509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms 
575511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
575511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
575511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
577967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
578782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
578787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.51ms 
578789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
578789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
578790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
581239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
581239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
582031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
582082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.51ms 
582083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
582083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
582084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
584517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
585334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
585344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.31ms 
585346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
585346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.9ns 
585346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
587801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
587801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
588617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
588620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
588622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
588622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
588622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
591072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
591885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
591901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.68ms 
591903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
591903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
591903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
594358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
595174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
595190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.16ms 
595191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
595191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
595192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
597657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
598474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
598492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.92ms 
598494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
598494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
598494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
600951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
601769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
601772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
601774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
601774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
601775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
604233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
605027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
605031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
605032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
605032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
605033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
607479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
608293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
608299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
608300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
608300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
608301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
610746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
611564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
611569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
611574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
611574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.8ns 
611575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
614034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
614853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
614920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.65ms 
614922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
614922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.6ns 
614923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
617385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
618203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
618229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.3ms 
618231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
618231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
618232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
620685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
621503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
621524     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.4ms 
621525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
621525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.1ns 
621526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
623984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
624803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
624805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 314.7ns 
624807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
624807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
624808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
627268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
628089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
628292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 193.45ms 
628295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
628295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.7ns 
628296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
630767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
630767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
631588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
631640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.34ms 
631641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
631641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
631642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
634098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
634916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
634918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 390.61ns 
634921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
634921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.6ns 
634922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
637372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
638189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
638191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 379.11ns 
638193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
638193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
638193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
640638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
641460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
641462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 376.61ns 
641464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
641464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
641465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
643910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
644726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
644728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 533.51ns 
644730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
644730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
644730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
647177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
647998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
648082     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
648095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 95.07ms 
648099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
648099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.3ns 
648100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
650595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
651390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
651439     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
651441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.28ms 
651443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
651443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
651444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
653950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
654773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
654774     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ns 
654800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
654836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
654853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
654858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
654863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
654866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
654867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
654869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
654872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
654874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
654876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
654877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
655078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
655080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
655081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
655083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
655083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
655227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
655228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
655231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
655234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
655236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
655236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
655423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
655425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
655426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
655427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
655429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
655435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
655564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
655566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
655567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
655568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
655568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
655569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
655577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
655577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
655578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
655580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
655582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
655583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
655591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
655592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
655593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
655594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
655595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
655595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
655748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
655749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
655752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
655910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
655911     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)'' 
655914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
655915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
655916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
655917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
655917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
655920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
655924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
655925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
655927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
655927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
655928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
656069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
656073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
656075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
656075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
656077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
656077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
656080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
656231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
656232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
656233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
656234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
656235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
656235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
656236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
656237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
656338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
656339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
656472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
656479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
656487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
656488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
656490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
656492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
656492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
656493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
656493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
656494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
656504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
656508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
656652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
656653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
656655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
656656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
656657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
656657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
656657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
656658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
656712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
656718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
656813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
656814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
656816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
656818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
656819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
656819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
656943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
656947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
656951     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)'' 
656952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
656954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
656954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
656955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
656956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
656964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
656969     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
656971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
656971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
657066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
657067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
657068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
657069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
657070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
657070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
657193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
657195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
657197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
657198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
657199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
657200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
657200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
657201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
657291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
657293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
657375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
657375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
657376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
657381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
657386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
657390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
657526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
657527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
657528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
657530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
657541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
657633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
661419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
661420     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)'' 
661425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
661426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
661426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
661427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
661428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
661436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
661437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
661438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
661438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
661439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
661533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
661537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
661538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
661539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
661540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
661541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
661542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
661636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
661638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
661639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
661641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
661642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
661642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
661643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
661644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
661720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
661721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
661802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
661806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
661811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
661812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
661813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
661814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
661825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
661910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
661912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
661913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
661914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
661986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
661995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
661996     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)'' 
661998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
661999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
661999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
662000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
662001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
662011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
662012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
662013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
662014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
662014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
662146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
662148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
662149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
662149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
662150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
662238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
662243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
662244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
662244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
662245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
662245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
662246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
662341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
662343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
662343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
662345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
662345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
662346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
662346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
662347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
662348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
662348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
662349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
662350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
662350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
662350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
662351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
662435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
662436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
662443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
662517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
662595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
662596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
662597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
662598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
662599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
662599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
662600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
662600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
662601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
662684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
662689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
662777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
662778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
662779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
662780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
662780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
662781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
662781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
662782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
662787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
662788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
662866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
662871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
662876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
662974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
662975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
662976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
662977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
662977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
662977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
662978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
662978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
663032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
663033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
663034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
663034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
663035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
663041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
663046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
663161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
663247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
663248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
663249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
663250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
663412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
663497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
663498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
666502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
666507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
666508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
666509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
666509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
666620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
666621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
666622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
666623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
666624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
666726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
669676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
672815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
672819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
672820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
672821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
672822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
672932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
672934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
672935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
672936     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)' ...' 
672937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
674042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
674042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.7ns 
674043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
676609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
676609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
677446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
677447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
677448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
677454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
677464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
677466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
677468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
677468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
677474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
677476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
677479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
677481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
677482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
677490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
677492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
677493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
677535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
677537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
677537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
677538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
677539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
677598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
677599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
677601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
677602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
677602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
677606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
677606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
677607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
677608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
677609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
677610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
677681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
677682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
677683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
677684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
677685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
677686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
677749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
677750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
677750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
677751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
677752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
677753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
677754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
677754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
677755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
677756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
677756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
677756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
677757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
677758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
677759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
677760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
677760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
677761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
677762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
677765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
677793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
677794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
677838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
677839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
677841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
677842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
677843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
677843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
677883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
677885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
677886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
677888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
677889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
677889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
677890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
677929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
677931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
677934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
677981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
678031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
678031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.41ns 
678032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
680557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
680557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
681435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
681516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.59ms