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

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

tests
0

failures
0

ignored
11m1.84s

duration
100%

successful

Tests

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

Standard output

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

1946       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1949       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1952       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1953       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3126       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8397       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.42s 
8476       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8511       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.9ns 
8525       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8525       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.1ns 
8530       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11389      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
11392      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12352      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12384      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.64ms 
12399      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12399      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.5ns 
12401      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15118      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
15119      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15997      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16012      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.76ms 
16015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16015      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.91ns 
16017      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18718      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
18719      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19583      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
19585      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19586      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 338.81ns 
19587      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22170      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
22171      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23040      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23054      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.71ms 
23062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23063      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 394.41ns 
23064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25585      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
25585      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26441      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26511      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.67ms 
26513      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26513      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.7ns 
26514      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29002      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
29003      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29869      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.43ms 
29874      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29874      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.8ns 
29875      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32351      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
32351      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33175      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 685.12ns 
33176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33176      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.8ns 
33177      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35653      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
35653      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36478      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36481      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 592.31ns 
36483      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36483      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 141.6ns 
36484      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38944      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
38944      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39766      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.91ns 
39769      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39769      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 350.91ns 
39770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42232      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
42233      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43041      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43044      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.01ns 
43047      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43047      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.31ns 
43048      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45546      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
45547      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46351      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46353      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 680.91ns 
46355      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46356      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.1ns 
46357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48884      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
48884      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49726      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.82ms 
49728      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49728      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 227.5ns 
49729      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52204      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
52204      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53003      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
53039      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.52ms 
53043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
53043      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 376.81ns 
53045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
55500      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
56304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56458      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 144.76ms 
56461      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56462      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.41ns 
56463      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58920      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
58921      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
59724      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
59730      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.19ms 
59732      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
59733      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.51ns 
59734      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62160      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
62161      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
62986      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
62990      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
62994      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
62994      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.41ns 
62996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65434      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
65434      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
66254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
66320      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.85ms 
66324      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
66324      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.7ns 
66325      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68788      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
68788      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
69610      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.11ms 
69615      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
69615      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 397.81ns 
69617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72109      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
72109      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
72915      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
72932      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.49ms 
72934      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
72935      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.3ns 
72939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75373      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
75374      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
76176      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
76191      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
76193      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
76193      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.5ns 
76194      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78635      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
78635      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
79436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
79450      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.92ms 
79452      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
79452      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.3ns 
79453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
81882      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
82696      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
82720      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.86ms 
82722      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
82722      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.7ns 
82723      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85142      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
85142      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
85939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
85942      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
85943      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
85943      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.7ns 
85944      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88363      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
88364      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
89161      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
89200      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.43ms 
89203      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
89203      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.51ns 
89204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91636      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
91636      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
92435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
92490      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.63ms 
92493      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
92493      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.51ns 
92494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94925      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
94925      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
95717      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
95760      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.63ms 
95762      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
95762      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144ns 
95763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98181      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
98182      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
98973      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
98980      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.41ms 
98982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
98982      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.1ns 
98982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
101445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
102239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
102260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.01ms 
102261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
102262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns 
102262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
104702     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
105497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
105509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.16ms 
105510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
105511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.7ns 
105511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
107920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
108715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
108723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.73ms 
108725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
108725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175ns 
108726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
111156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
111950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
111958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.03ms 
111960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
111960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
111961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
114389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
115187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
115195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.36ms 
115198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
115199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.21ns 
115200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
117631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
118439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
118443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
118445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
118446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.21ns 
118447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
120879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
121671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
121682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.98ms 
121684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
121684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.8ns 
121685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
124104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
124892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
124950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.66ms 
124953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
124953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335.41ns 
124955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
127380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
128175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
128195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.03ms 
128197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
128198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.51ns 
128199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
130695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
131515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
131537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.22ms 
131539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
131539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.8ns 
131540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
133977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
134777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
134801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.78ms 
134802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
134802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.7ns 
134803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
137250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
138047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
138081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.6ms 
138083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
138084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.9ns 
138086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
140598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
141392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
141436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.73ms 
141438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
141438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.8ns 
141439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
143910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
144683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
144686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
144688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
144688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
144689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
147119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
147914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
147919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
147921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
147921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
147923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
150340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
151125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
151134     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ms 
151136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
151136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
151137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
153539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
154330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
154339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.47ms 
154340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
154340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
154341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
156744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
157532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
157551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.24ms 
157553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
157553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
157556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
159963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
160753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
160763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.25ms 
160766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
160766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
160767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
163179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
163983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
163997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
164005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
164005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.9ns 
164006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
166585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
167373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
167381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.15ms 
167385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
167386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.07ms 
167387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
169799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
170585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
170590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
170592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
170592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.11ns 
170593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
173048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
173836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
173910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.44ms 
173912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
173912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.3ns 
173913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
176352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
177139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
177225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.77ms 
177227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
177227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.9ns 
177228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
179701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
180466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
180470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
180472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
180472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
180472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
182908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
183670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
183709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.43ms 
183711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
183711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.81ns 
183712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
186196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
186959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
186989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.81ms 
186991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
186991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.3ns 
186991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
189415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
190178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
190180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
190182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
190182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
190183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
192614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
193372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
193518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 135.53ms 
193521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
193521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.11ns 
193522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
195967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
196736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
196753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.71ms 
196754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
196755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
196755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
199177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
199935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
199943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.52ms 
199944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
199945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
199945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
202348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
203110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
203127     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.4ms 
203129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
203129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.7ns 
203130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
205565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
206322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
206336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ms 
206338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
206338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
206339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
208750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
209507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
209511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
209512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
209512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
209513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
211959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
212726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
212731     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
212732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
212733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
212733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
215168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
215933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
215957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.66ms 
215960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
215960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 284.7ns 
215961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
218416     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
219190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
219206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.71ms 
219208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
219208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
219209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
221681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
222453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
222469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.76ms 
222471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
222471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.9ns 
222472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
224942     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
225708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
225711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
225713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
225713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.2ns 
225714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
228156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
228918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
228922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.75ms 
228924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
228924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
228924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
231462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
232223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
232229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.75ms 
232230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
232230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
232231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
234655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
235415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
235418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
235419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
235420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
235420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
237841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
238604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
238607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 742.91ns 
238608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
238608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
238609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
241039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
241799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
241803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
241804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
241804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
241805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
244238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
244997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
245000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.02ms 
245001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
245001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
245002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
247422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
248187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
248241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.22ms 
248246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
248246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245.91ns 
248247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
250767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
251524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
251570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.73ms 
251573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
251573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.81ns 
251574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
254026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
254788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
254818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.11ms 
254820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
254820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
254821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
257274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
258067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
258109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.14ms 
258110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
258110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
258111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
260533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
261297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
261328     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.63ms 
261329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
261329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
261330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
263764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
264524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
264576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.89ms 
264577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
264577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
264578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
267007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
267765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
267796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.33ms 
267798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
267798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.4ns 
267799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
270233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
271002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
271023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.02ms 
271025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
271025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
271026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
273513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
274271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
274297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.33ms 
274298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
274298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
274299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
276732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
277493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
277514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.79ms 
277516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
277516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
277516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
279930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
280688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
280717     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.81ms 
280719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
280719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.7ns 
280720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
283138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
283896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
283921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.89ms 
283922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
283923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
283923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
286352     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
287112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
287138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.83ms 
287140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
287140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
287140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
289555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
290318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
290345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.54ms 
290347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
290347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.7ns 
290347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
292788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
293547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
293569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.3ms 
293570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
293570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
293571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
296094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
296852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
296879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.06ms 
296880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
296880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
296881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
299311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
300071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
300097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.6ms 
300098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
300098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
300099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
302532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
303297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
303305     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ms 
303307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
303307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
303308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
305746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
306516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
306535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.91ms 
306537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
306537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
306537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
309003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
309766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
309771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
309772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
309772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
309773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
312228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
312991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
312993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 697.51ns 
312995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
312995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
312996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
315526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
316287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
316290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 806.62ns 
316291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
316291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
316292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
318761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
319526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
319534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
319535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
319536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
319536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
321960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
322719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
322725     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
322727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
322727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
322727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
325168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
325928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
325940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.93ms 
325942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
325942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
325942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
328360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
329121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
329125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
329126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
329126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
329127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
331562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
332320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
332322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 570.41ns 
332323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
332323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
332324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
334755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
335517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
335527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
335529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
335529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.21ns 
335530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
338022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
338780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
338783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 728.41ns 
338784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
338784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
338785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
341196     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
341956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
341958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 619.61ns 
341959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
341959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
341960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
344430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
345190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
345192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 646.91ns 
345193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
345193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
345194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
347615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
348381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
348385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
348386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
348387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
348387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
350812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
351578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
351587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.32ms 
351589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
351589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
351590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
354024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
354787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
354791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
354792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
354792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
354793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
357223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
358011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
358019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
358020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
358020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
358021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
360438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
361199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
361203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
361205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
361205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
361205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
363627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
364387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
364403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.24ms 
364404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
364404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
364405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
366825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
367585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
367588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
367589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
367590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
367590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
370018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
370781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
370784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
370786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
370786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
370787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
373220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
373985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
373990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
373991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
373991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
373992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
376422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
377183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
377201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.99ms 
377202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
377202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
377203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
379637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
380399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
380404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.11ns 
380406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
380406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
380407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
382837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
383604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
383644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.17ms 
383646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
383646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
383647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
386103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
386870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
386873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
386875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
386875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
386875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
389325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
390092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
390115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.59ms 
390116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
390116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
390117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
392577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
393344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
393366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.98ms 
393367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
393367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
393368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
395814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
396577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
396602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.66ms 
396603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
396603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
396604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
399034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
399798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
399800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 681.61ns 
399802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
399802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
399802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
402239     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
403003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
403009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.01ms 
403011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
403011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
403012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
405624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
406418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
406422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
406423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
406423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
406424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
408847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
409627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
409630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 901.92ns 
409631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
409631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
409632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
412063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
412826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
412828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 888.72ns 
412830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
412830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
412830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
415247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
416015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
416019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
416020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
416020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
416021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
418446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
419207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
419210     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
419211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
419211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
419212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
421627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
422396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
422406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.52ms 
422407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
422407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
422408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
424832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
425593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
425605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.77ms 
425606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
425606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
425607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
428040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
428812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
428830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.84ms 
428834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
428834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
428837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
431276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
432046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
432058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.47ms 
432059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
432059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
432060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
434497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
435269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
435274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.01ms 
435275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
435275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
435276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
437709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
438486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
438492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms 
438494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
438494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
438494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
440919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
441691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
441693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 732.71ns 
441695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
441695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
441697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
444189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
444981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
444984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
444985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
444985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
444986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
447399     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
448197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
448199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 895.02ns 
448201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
448201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
448201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
450636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
451441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
451453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.17ms 
451454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
451454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
451455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
453872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
454672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
454676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
454677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
454677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83ns 
454678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
457098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
457898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
457905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
457906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
457906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
457907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
460325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
461133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
461135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 826.22ns 
461137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
461137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
461137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
463561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
464360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
464363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 688.61ns 
464364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
464364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
464365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
466822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
467598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
467602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
467604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
467604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
467605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
470023     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
470788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
470791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
470793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
470793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
470793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
473222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
474019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
474025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
474027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
474027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.1ns 
474028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
476451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
477277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
477280     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
477282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
477282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
477282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
479715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
480507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
480512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
480513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
480513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
480514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
482900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
483690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
483693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
483695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
483695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
483695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
486077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
486870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
486881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.85ms 
486883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
486883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.6ns 
486883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
489317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
490081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
490083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 699.81ns 
490084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
490084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
490085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
492569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
493364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
493371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.25ms 
493372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
493372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
493373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
495781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
496577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
496579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 928.32ns 
496581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
496581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
496581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
498977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
499769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
499771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 813.32ns 
499772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
499773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
499773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
502171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
502966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
502971     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.33ms 
502973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
502973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.6ns 
502974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
505409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
506182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
506185     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
506186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
506186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
506187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
508622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
509424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
509428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
509429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
509429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
509430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
511846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
512644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
512648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
512649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
512649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
512650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
515075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
515878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
515884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
515885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
515885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
515887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
518357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
519162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
519177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.81ms 
519179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
519179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
519179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
521591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
522383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
522398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.68ms 
522400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
522400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
522400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
524799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
525604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
525615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.66ms 
525616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
525616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
525617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
528029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
528795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
528805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.87ms 
528807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
528807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
528807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
531238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
532048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
532074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.58ms 
532076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
532076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
532076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
534578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
534578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
535375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
535400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.14ms 
535401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
535402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
535402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
537844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
537844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
538617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
538644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.93ms 
538645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
538645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
538646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
541062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
541852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
541866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.23ms 
541867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
541867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
541868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
544272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
545062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
545092     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.77ms 
545094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
545094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
545095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
547508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
548278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
548356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.85ms 
548357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
548358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
548358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
550742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
551543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
551583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.27ms 
551586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
551586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.5ns 
551587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
553988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
554757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
554801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.98ms 
554802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
554802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
554803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
557206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
557995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
558040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.43ms 
558041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
558041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
558042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
560421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
561212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
561333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.51ms 
561335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
561335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
561335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
563746     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
564535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
564543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms 
564544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
564544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
564545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
566925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
567713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
567721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
567722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
567722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
567723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
570117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
570909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
570915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.87ms 
570916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
570916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
570917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
573300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
574090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
574108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.3ms 
574110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
574110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
574110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
576510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
577276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
577288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.96ms 
577289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
577289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
577290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
579683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
580470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
580473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
580474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
580475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
580475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
582881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
583649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
583668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.56ms 
583669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
583669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
583670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
586084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
586873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
586890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.59ms 
586892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
586892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
586892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
589302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
590070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
590090     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.81ms 
590091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
590091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
590092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
592491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
593312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
593316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
593317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
593317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.6ns 
593318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
595757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
596524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
596527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
596529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
596529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
596530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
598930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
599720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
599726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
599728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
599728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
599728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
602142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
602920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
602926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
602928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
602928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
602929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
605343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
606136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
606205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 63.44ms 
606207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
606207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
606207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
608686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
609475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
609501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.8ms 
609504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
609504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.3ns 
609505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
611894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
612686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
612709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.1ms 
612710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
612710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
612711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
615111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
615899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
615901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 301.91ns 
615903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
615903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.1ns 
615905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
618297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
619085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
619283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 188.76ms 
619285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
619286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.5ns 
619287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
621709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
622501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
622553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.94ms 
622554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
622554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
622555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
624966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
625759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
625761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 360.81ns 
625763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
625763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
625764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
628168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
628937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
628939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 365.21ns 
628940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
628940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
628941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
631327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
632118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
632119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 369.51ns 
632121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
632121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
632121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
634514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
635300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
635302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 511.11ns 
635303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
635304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
635304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
637698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
638491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
638594     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
638611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 117.25ms 
638613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
638614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.2ns 
638615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
641037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
641827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
641881     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
641882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.55ms 
641884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
641884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
641885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
644290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
645088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
645089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ns 
645116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
645153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
645170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
645173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
645180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
645182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
645183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
645185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
645193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
645194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
645196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
645197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
645349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
645350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
645351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
645352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
645353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
645465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
645472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
645473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
645476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
645477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
645479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
645634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
645637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
645638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
645638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
645639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
645641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
645767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
645769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
645770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
645771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
645772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
645773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
645780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
645781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
645781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
645784     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
645785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
645785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
645794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
645795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
645796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
645799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
645800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
645801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
645954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
645955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
645957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
646073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
646075     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)'' 
646077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
646079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
646079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
646080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
646081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
646083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
646087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
646088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
646089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
646090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
646090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
646197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
646200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
646202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
646202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
646203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
646204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
646205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
646314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
646316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
646316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
646318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
646319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
646319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
646320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
646322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
646405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
646406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
646481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
646485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
646490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
646491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
646494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
646496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
646496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
646497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
646497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
646498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
646506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
646511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
646588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
646590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
646592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
646593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
646594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
646594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
646595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
646598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
646643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
646648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
646746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
646748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
646750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
646751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
646752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
646753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
646872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
646876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
646879     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)'' 
646881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
646882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
646883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
646884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
646884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
646892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
646900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
646901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
646902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
646984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
646986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
646987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
646988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
646988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
646989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
647084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
647086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
647087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
647089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
647089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
647090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
647090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
647091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
647167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
647168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
647236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
647236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
647237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
647241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
647244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
647248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
647359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
647360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
647361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
647362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
647371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
647492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
651010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
651012     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)'' 
651017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
651017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
651018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
651019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
651020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
651028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
651029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
651030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
651031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
651031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
651123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
651127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
651131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
651132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
651133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
651133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
651135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
651228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
651230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
651231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
651234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
651235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
651236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
651236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
651238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
651320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
651322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
651403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
651407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
651412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
651413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
651414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
651416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
651425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
651505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
651507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
651508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
651509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
651578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
651587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
651588     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)'' 
651590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
651591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
651592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
651592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
651593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
651603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
651605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
651606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
651606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
651607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
651690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
651692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
651693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
651694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
651695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
651781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
651785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
651787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
651788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
651788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
651789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
651790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
651884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
651886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
651887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
651888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
651889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
651890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
651890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
651891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
651892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
651893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
651894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
651895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
651895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
651896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
651897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
652026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
652028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
652033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
652106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
652183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
652184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
652186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
652186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
652187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
652188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
652188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
652189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
652190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
652270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
652276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
652360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
652361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
652362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
652363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
652364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
652364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
652365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
652366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
652371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
652371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
652446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
652452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
652457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
652551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
652553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
652554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
652555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
652555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
652556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
652556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
652557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
652609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
652611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
652612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
652612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
652613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
652619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
652624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
652736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
652820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
652821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
652822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
652823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
652981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
653068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
653069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
655984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
655990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
655991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
655992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
655992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
656101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
656103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
656104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
656105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
656105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
656207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
658993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
661985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
661990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
661992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
661992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
661993     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
662101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
662102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
662104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
662105     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)' ...' 
662107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
663210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
663210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.5ns 
663211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
665685     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
666500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
666501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ns 
666502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
666507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
666519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
666521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
666523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
666523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
666527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
666528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
666531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
666533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
666534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
666542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
666543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
666544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
666586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
666587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
666587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
666588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
666588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
666648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
666649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
666650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
666651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
666652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
666656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
666657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
666657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
666658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
666659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
666660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
666738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
666740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
666740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
666742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
666743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
666743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
666821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
666822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
666822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
666823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
666824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
666825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
666825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
666826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
666827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
666827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
666828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
666828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
666829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
666830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
666830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
666831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
666831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
666832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
666833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
666836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
666870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
666871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
666917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
666919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
666920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
666922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
666922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
666923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
666961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
666963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
666964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
666966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
666967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
666968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
666968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
667008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
667011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
667014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
667062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
667114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
667114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.2ns 
667115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
669541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
670350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
670382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.85ms