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

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

tests
0

failures
0

ignored
11m5.91s

duration
100%

successful

Tests

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

Standard output

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

1606       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1609       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1611       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1611       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2757       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8019       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.18s 
8087       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8120       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31ns 
8132       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8134       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.6ms 
8138       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10940      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
10942      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11891      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11918      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.39ms 
11929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11929      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.9ns 
11931      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14662      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
14663      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15572      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15597      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.12ms 
15600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15600      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.7ns 
15605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18300      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
18300      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19178      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19185      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.05ms 
19187      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19187      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.9ns 
19189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21795      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
21795      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22678      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22691      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.14ms 
22696      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22697      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 523.41ns 
22698      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25283      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
25284      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26105      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26144      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.86ms 
26146      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26147      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.6ns 
26148      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28676      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
28676      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29478      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29498      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.31ms 
29501      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29501      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.1ns 
29502      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32006      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
32006      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32834      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 665.91ns 
32836      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32837      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327ns 
32838      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35331      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
35331      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36198      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 607.21ns 
36201      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36201      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.3ns 
36202      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38679      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
38680      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39506      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39508      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 602.81ns 
39510      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39510      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
39511      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41983      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
41983      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42817      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 715.21ns 
42820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42820      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.8ns 
42822      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45306      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
45306      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46095      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 597.61ns 
46097      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46097      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
46098      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48597      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
48597      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49494      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 81.93ms 
49496      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49496      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.7ns 
49497      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51989      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
51989      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52832      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.05ms 
52834      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52834      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.8ns 
52835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55290      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
55291      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
56103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56241      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 128.75ms 
56245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56246      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 563.71ns 
56247      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58704      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
58705      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59523      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59528      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 
59531      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59531      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.5ns 
59532      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61981      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
61982      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62796      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62799      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
62802      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62803      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.9ns 
62804      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65272      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
65273      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
66057      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
66096      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.95ms 
66098      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
66099      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 311.6ns 
66100      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68579      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
68579      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69386      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69402      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.96ms 
69403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69404      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.2ns 
69405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71859      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
71859      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
72664      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
72688      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.23ms 
72689      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
72690      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.5ns 
72690      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75136      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
75136      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
75940      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
75955      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.32ms 
75956      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
75956      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
75957      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78394      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
78394      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
79221      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
79236      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.48ms 
79237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
79237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.2ns 
79238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81700      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
81701      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
82481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
82514      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.57ms 
82517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82517      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.2ns 
82518      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84990      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
84990      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
85813      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
85816      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
85818      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
85819      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.4ns 
85820      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88282      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
88283      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
89087      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
89128      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.46ms 
89131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
89131      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.5ns 
89132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91589      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
91589      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
92398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
92454      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.83ms 
92457      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
92457      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.2ns 
92458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94895      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
94895      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
95696      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
95739      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.53ms 
95741      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
95741      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
95741      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98197      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
98198      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
98980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
98994      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.07ms 
98996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
98996      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.2ns 
98997      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
101464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
102248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
102264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.6ms 
102265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
102265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.3ns 
102266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
104753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
105553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
105564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.21ms 
105565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
105565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
105566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
108055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
108866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
108875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.41ms 
108878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
108878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 586.91ns 
108880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
111312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
112118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
112131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.02ms 
112132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
112133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
112134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
114577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
115383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
115390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.81ms 
115391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
115391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
115392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
117855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
118633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
118637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
118638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
118638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.5ns 
118639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
121115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
121916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
121926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.55ms 
121928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
121928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.9ns 
121929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
124368     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
125177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
125250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.33ms 
125255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
125255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 
125256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
127718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
128521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
128538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.04ms 
128539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
128539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns 
128540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
130973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
131774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
131791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.79ms 
131792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
131792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
131793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
134249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
135030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
135053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.66ms 
135055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
135056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.6ns 
135057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
137510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
138284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
138300     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13ms 
138301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
138301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
138302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
140752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
141552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
141589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.79ms 
141591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
141591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.6ns 
141593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
144035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
144835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
144838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
144840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
144840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.6ns 
144841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
147287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
148097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
148102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.43ms 
148104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
148104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.9ns 
148105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
150546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
151344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
151352     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.52ms 
151353     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
151353     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
151354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
153809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
154587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
154595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.88ms 
154596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
154596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
154597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
157048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
157844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
157861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.7ms 
157862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
157863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
157863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
160291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
161087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
161095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.81ms 
161096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
161096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
161097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
163517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
164334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
164337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
164338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
164339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.1ns 
164340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
166760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
167577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
167581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
167583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
167583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
167584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
170024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
170802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
170809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
170812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
170812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
170813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
173274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
174051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
174120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.66ms 
174122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
174122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.4ns 
174123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
176594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
177394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
177473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.54ms 
177475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
177475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
177476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
179911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
180710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
180713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
180714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
180714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
180715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
183150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
183946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
183983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.19ms 
183985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
183985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.9ns 
183986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
186402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
187199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
187227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.63ms 
187228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
187228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
187229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
189685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
190460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
190462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
190463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
190463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
190465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
192912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
193712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
193851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 127.17ms 
193854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
193854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.4ns 
193855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
196285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
197085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
197096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.76ms 
197097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
197097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
197098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199526     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
199526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
200324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
200332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.02ms 
200333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
200333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
200334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
202756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
203553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
203569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.86ms 
203570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
203570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
203571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
206007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
206779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
206791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.57ms 
206794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
206794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.3ns 
206795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
209253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
210042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
210046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
210048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
210048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.6ns 
210049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
212458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
213252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
213257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.72ms 
213258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
213258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
213259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
215673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
216468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
216491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.68ms 
216492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
216492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
216493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
218918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
219726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
219743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.42ms 
219745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
219745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
219746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
222200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
222974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
222990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ms 
222992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
222992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.4ns 
222993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
225439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
226213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
226216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
226217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
226217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
226218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
228666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
229462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
229466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
229467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
229467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
229468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
231889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
232684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
232689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
232691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
232691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
232691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
235109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
235904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
235907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
235909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
235909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.9ns 
235910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
238328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
239145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
239147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 695.81ns 
239148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
239148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
239149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
241588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
242359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
242362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
242364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
242364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
242364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
244804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
245602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
245605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
245606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
245606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
245606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
248017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
248811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
248853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.15ms 
248855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
248855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.2ns 
248856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
251269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
252063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
252098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.96ms 
252099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
252099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
252100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
254512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
255304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
255335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.78ms 
255336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
255336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
255337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
257778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
258551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
258595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.03ms 
258597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
258597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
258598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
261037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
261810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
261840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.85ms 
261841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
261841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
261842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
264290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
265086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
265134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.26ms 
265135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
265136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
265136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
267563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
268356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
268381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.67ms 
268382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
268382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
268383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
270808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
271604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
271623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.19ms 
271624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
271624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
271625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
274040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
274834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
274857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.45ms 
274858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
274858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
274859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
277299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
278073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
278092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.15ms 
278093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
278094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
278094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
280548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
281341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
281368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.62ms 
281369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
281369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
281370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
283790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
284587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
284612     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.7ms 
284614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
284614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
284614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
287028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
287824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
287849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.26ms 
287850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
287850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
287851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
290274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
291072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
291096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.21ms 
291097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
291097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
291098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
293541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
294318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
294339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.09ms 
294340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
294340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
294341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
296786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
297583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
297606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.9ms 
297608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
297608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
297608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
300024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
300820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
300851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.16ms 
300852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
300852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
300853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
303295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
304097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
304104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
304105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
304105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
304106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
306528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
307328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
307345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.56ms 
307346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
307346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
307347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
309790     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
310567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
310571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
310572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
310572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
310572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
313011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
313785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
313788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.61ns 
313789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
313789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
313790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
316225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
317023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
317026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 709.91ns 
317027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
317027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
317027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
319448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
320249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
320264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.31ms 
320269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
320269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 439.61ns 
320271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
322691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
323496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
323505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.12ms 
323506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
323506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
323507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
325924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
326726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
326738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.82ms 
326739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
326739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
326740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
329186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
329963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
329966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.93ms 
329967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
329967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50ns 
329968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
332409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
333204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
333206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 526.81ns 
333207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
333208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
333208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
335632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
336432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
336441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
336443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
336443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196ns 
336444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
338861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
339660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
339662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 665.51ns 
339664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
339664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
339664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
342073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
342867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
342869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.21ns 
342870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
342870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
342871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
345299     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
346072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
346073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 580.71ns 
346075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
346075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
346075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
348505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
349277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
349280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
349281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
349282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
349282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
351706     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
352502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
352511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.52ms 
352512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
352512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
352513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
354921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
355716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
355719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
355720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
355720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
355721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
358129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
358923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
358930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
358931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
358931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
358932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
361342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
362135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
362139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
362140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
362140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
362141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
364579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
365356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
365371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.8ms 
365373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
365373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
365373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
367813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
368616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
368619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
368620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
368620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
368621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
371044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
371843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
371848     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
371849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
371849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
371849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
374272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
375071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
375075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
375076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
375076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
375077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
377497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
378299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
378315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.78ms 
378317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
378318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201ns 
378318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
380740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
381537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
381541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 567.11ns 
381543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
381543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
381543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
383977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
384752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
384789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.95ms 
384791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
384791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
384791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
387229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
388027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
388030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
388032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
388032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
388032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
390458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
391254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
391275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.02ms 
391276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
391276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
391277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
393693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
394490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
394509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.22ms 
394511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
394511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
394512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
396956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
397730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
397753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.26ms 
397755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
397755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
397755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
400195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
400971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
400973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 571.81ns 
400975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
400975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
400975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
403413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
404208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
404213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
404214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
404214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
404215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
406626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
407422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
407425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
407426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
407426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
407427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
409846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
410645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
410648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.92ns 
410649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
410649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
410650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
413091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
413900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
413902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 833.21ns 
413906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
413906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
413907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
416340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
417147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
417150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
417151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
417151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51ns 
417152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
419567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
420371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
420373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
420375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
420375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
420375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
422807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
423587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
423596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.02ms 
423598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
423598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
423598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
426043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
426845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
426856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.39ms 
426857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
426857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
426858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
429279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
430082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
430095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ms 
430096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
430096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.6ns 
430097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
432540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
433326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
433338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.43ms 
433339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
433339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
433340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
435780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
436596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
436605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.49ms 
436606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
436606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
436607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
439028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
439838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
439845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.45ms 
439846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
439846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
439846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
442293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
443080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
443082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 675.41ns 
443083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
443083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
443084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
445523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
446338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
446340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
446342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
446342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
446342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
448763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
449573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
449576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 945.21ns 
449577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
449577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
449578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
452022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
452810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
452820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.25ms 
452821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
452821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
452822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
455266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
456076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
456079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
456081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
456081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
456081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
458499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
459310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
459316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.41ms 
459318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
459318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.8ns 
459319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
461752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
462562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
462564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 725.91ns 
462565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
462565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
462565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
464983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
465793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
465795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.91ns 
465796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
465796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
465797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
468226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
469040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
469044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
469045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
469045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
469046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
471458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
472267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
472270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
472271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
472271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
472272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
474710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
475498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
475501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
475502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
475502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
475503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
477937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
478745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
478748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
478749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
478749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
478750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
481191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
481979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
481984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.48ms 
481985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
481985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
481986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
484420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
485232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
485235     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
485236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
485236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
485237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
487674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
488461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
488471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.18ms 
488473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
488473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
488473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
490905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
491717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
491719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.21ns 
491720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
491720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
491721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
494154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
494941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
494948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
494949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
494949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
494950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
497385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
498193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
498196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 833.81ns 
498197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
498197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
498197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
500637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
501424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
501427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 749.71ns 
501428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
501428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57ns 
501428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
503864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
504672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
504677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
504679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
504679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.5ns 
504679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
507118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
507926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
507929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
507930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
507930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
507931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
510356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
511166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
511170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.73ms 
511171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
511171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.9ns 
511171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
513607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
514416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
514420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
514421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
514421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.2ns 
514421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
516839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
517648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
517652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.08ms 
517653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
517654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
517654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
520088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
520896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
520910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.65ms 
520911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
520911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
520912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
523344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
524150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
524165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.61ms 
524166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
524166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
524166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
526582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
527388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
527398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.96ms 
527399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
527399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
527400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
529831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
530637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
530650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.81ms 
530652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
530652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.5ns 
530653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
533086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
533874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
533926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.06ms 
533927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
533927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
533928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
536335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
537145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
537169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.58ms 
537170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
537170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
537171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
539608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
540419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
540441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.37ms 
540442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
540442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
540443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
542882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
543691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
543705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.43ms 
543706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
543706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
543706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
546128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
546936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
546966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.94ms 
546968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
546968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
546969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
549403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
550212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
550256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.58ms 
550257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
550257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
550258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
552694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
553504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
553540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.54ms 
553541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
553541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
553542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
555977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
556787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
556827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.23ms 
556828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
556828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
556829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
559254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
560062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
560103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.15ms 
560105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
560105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
560106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
562539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
563348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
563461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 104.73ms 
563464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
563464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.4ns 
563464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
565915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
565915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
566729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
566739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
566740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
566740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
566741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
569168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
569975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
569982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.33ms 
569983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
569983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
569984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
572413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
573222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
573227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.28ms 
573228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
573228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
573229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
575670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
576456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
576473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.26ms 
576474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
576475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
576475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
578902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
578902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
579710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
579720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.19ms 
579721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
579721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
579722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
582148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
582955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
582958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
582959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
582959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
582960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
585387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
586195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
586211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.67ms 
586212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
586212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
586213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
588644     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
589452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
589468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.01ms 
589469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
589469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
589470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
591903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
592715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
592735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.95ms 
592737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
592737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.2ns 
592738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
595177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
595990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
595993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 944.41ns 
595994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
595994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
595995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
598427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
599239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
599242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
599243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
599244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
599244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
601680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
602467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
602474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.37ms 
602475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
602475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
602476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
604905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
605713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
605719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
605720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
605720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
605721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
608153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
608961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
609029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.73ms 
609031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
609032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.1ns 
609033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
611476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
612288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
612313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.54ms 
612315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
612315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.4ns 
612316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
614758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
615568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
615589     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.35ms 
615590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
615590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
615590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
618028     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
618842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
618844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 263.5ns 
618846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
618846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.7ns 
618847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
621280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
622086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
622336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 237.47ms 
622337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
622338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
622338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
624768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
625580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
625628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.63ms 
625630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
625630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
625630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
628062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
628872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
628874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 332.8ns 
628876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
628876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
628877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
631309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
632121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
632123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 337.3ns 
632124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
632124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
632125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
634555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
635366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
635368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 362.31ns 
635369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
635369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
635370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
637805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
638615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
638617     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 458.2ns 
638618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
638618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
638619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
641046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
641857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
641944     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
641959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.16ms 
641961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
641961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
641964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
644413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
645229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
645277     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
645278     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.94ms 
645279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
645279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
645280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
647727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
648537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
648539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.9ns 
648564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
648596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
648611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
648615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
648620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
648622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
648623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
648624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
648627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
648629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
648630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
648631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
648841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
648842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
648843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
648845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
648846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
648975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
648977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
648978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
648979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
648980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
648981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
649152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
649154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
649155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
649156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
649157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
649158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
649275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
649277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
649278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
649279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
649280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
649281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
649287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
649288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
649289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
649291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
649292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
649292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
649299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
649300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
649300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
649301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
649302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
649303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
649431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
649432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
649434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
649549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
649551     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)'' 
649553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
649554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
649556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
649557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
649558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
649559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
649562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
649564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
649565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
649565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
649566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
649669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
649673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
649675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
649676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
649677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
649678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
649679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
649826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
649830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
649831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
649833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
649834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
649834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
649835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
649837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
649921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
649922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
650005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
650008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
650013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
650014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
650016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
650017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
650018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
650019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
650019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
650020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
650028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
650031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
650118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
650119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
650121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
650123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
650123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
650124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
650124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
650125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
650174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
650180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
650265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
650267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
650269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
650270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
650271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
650271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
650405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
650409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
650413     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)'' 
650415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
650416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
650417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
650417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
650418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
650427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
650432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
650433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
650435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
650538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
650540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
650541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
650541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
650542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
650543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
650644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
650646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
650646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
650649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
650650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
650650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
650651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
650652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
650730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
650731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
650801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
650802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
650803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
650807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
650811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
650815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
650931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
650932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
650933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
650934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
650945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
651024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
654522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
654524     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)'' 
654529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
654530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
654531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
654532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
654532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
654540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
654541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
654542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
654543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
654544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
654638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
654641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
654643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
654643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
654645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
654645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
654646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
654737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
654739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
654740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
654741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
654741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
654742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
654743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
654744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
654816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
654817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
654888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
654892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
654896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
654897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
654897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
654898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
654908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
654986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
654987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
654988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
654989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
655058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
655066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
655067     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)'' 
655070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
655071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
655071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
655072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
655072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
655083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
655086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
655088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
655088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
655089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
655173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
655175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
655176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
655177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
655177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
655265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
655270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
655271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
655271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
655272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
655273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
655273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
655368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
655370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
655371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
655372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
655373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
655373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
655374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
655375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
655376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
655377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
655378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
655378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
655379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
655379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
655380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
655464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
655466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
655472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
655546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
655623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
655625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
655626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
655627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
655628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
655628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
655629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
655629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
655630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
655715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
655721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
655853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
655854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
655855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
655856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
655856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
655857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
655857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
655858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
655863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
655864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
655940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
655945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
655950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
656045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
656047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
656047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
656048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
656048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
656049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
656049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
656050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
656102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
656103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
656103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
656105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
656106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
656111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
656116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
656227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
656312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
656313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
656313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
656314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
656474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
656558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
656559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
659427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
659432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
659433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
659433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
659434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
659542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
659543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
659544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
659545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
659545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
659646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
662451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
665389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
665393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
665394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
665394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
665395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
665504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
665505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
665506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
665507     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)' ...' 
665508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
666584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
666584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127ns 
666585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
669138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
669975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
669977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ns 
669977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
669983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
669993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
669995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
669996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
669997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
670001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
670002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
670004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
670006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
670007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
670016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
670017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
670017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
670066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
670067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
670067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
670068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
670068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
670135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
670135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
670136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
670137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
670137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
670141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
670141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
670142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
670143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
670143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
670144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
670228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
670228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
670229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
670230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
670231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
670231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
670317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
670318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
670319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
670319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
670320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
670321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
670321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
670322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
670323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
670323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
670324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
670324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
670325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
670325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
670326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
670326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
670327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
670328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
670329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
670331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
670369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
670370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
670432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
670433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
670434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
670436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
670436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
670437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
670489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
670491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
670492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
670494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
670495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
670496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
670496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
670542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
670545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
670548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
670606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
670662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
670662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.6ns 
670663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
673164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
674024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
674054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.55ms