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

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

tests
0

failures
0

ignored
10m40.81s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.113s passed
powPositiveConcrete data()[101] 3.078s passed
powGeq1Concrete data()[102] 3.082s passed
pow2InIntLower data()[103] 3.101s passed
pow2InIntUpper data()[104] 3.085s passed
logSelfConcrete data()[105] 3.093s passed
log1Concrete data()[106] 3.100s passed
logProduct data()[107] 3.151s passed
logTimesBaseConcrete data()[108] 3.216s passed
logProdIdentity data()[109] 3.234s passed
moduloByteIsInByte data()[10] 3.171s passed
logProdIdentityConcrete data()[110] 3.214s passed
logPowIdentity data()[111] 3.232s passed
logPowIdentityConcrete data()[112] 3.091s passed
logPositive data()[113] 3.121s passed
logPositiveConcrete data()[114] 3.115s passed
logMono data()[115] 3.125s passed
logMonoConcrete data()[116] 3.089s passed
powLogLess data()[117] 3.130s passed
powLogMore2 data()[118] 3.115s passed
logLessThanPow data()[119] 3.109s passed
moduloCharIsInChar data()[11] 3.222s passed
logLessThanPowConcrete data()[120] 3.100s passed
logSqueeze data()[121] 3.085s passed
ifthenelse_equals data()[122] 3.110s passed
ifthenelse_equals_1 data()[123] 3.096s passed
ifthenelse_equals_2 data()[124] 3.088s passed
disjointWithSingleton1 data()[125] 3.111s passed
disjointWithSingleton2 data()[126] 3.088s passed
disjointArrayRanges data()[127] 3.191s passed
disjointArrayRangeAllFields1 data()[128] 3.104s passed
disjointArrayRangeAllFields2 data()[129] 3.114s passed
div_unique1 data()[12] 3.233s passed
seqSelfDefinition data()[130] 3.093s passed
seqOutsideValue data()[131] 3.153s passed
castedGetAny data()[132] 3.180s passed
seqGetAlphaCast data()[133] 3.220s passed
getOfSeqSingleton data()[134] 3.092s passed
getOfSeqSingletonConcrete data()[135] 3.094s passed
getOfSeqConcat data()[136] 3.094s passed
getOfSeqSub data()[137] 3.124s passed
getOfSeqReverse data()[138] 3.094s passed
lenOfSeqEmpty data()[139] 3.105s passed
div_unique2 data()[13] 3.244s passed
lenOfSeqSingleton data()[140] 3.140s passed
lenOfSeqConcat data()[141] 3.158s passed
lenOfSeqSub data()[142] 3.111s passed
lenOfSeqReverse data()[143] 3.096s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.081s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.109s passed
getOfSeqSingletonEQ data()[146] 3.107s passed
getOfSeqConcatEQ data()[147] 3.122s passed
getOfSeqSubEQ data()[148] 3.106s passed
getOfSeqReverseEQ data()[149] 3.107s passed
div_exists data()[14] 3.455s passed
lenOfSeqEmptyEQ data()[150] 3.101s passed
lenOfSeqSingletonEQ data()[151] 3.098s passed
lenOfSeqConcatEQ data()[152] 3.104s passed
lenOfSeqSubEQ data()[153] 3.087s passed
lenOfSeqReverseEQ data()[154] 3.100s passed
getOfSeqDefEQ data()[155] 3.113s passed
lenOfSeqDefEQ data()[156] 3.101s passed
seqConcatWithSeqEmpty1 data()[157] 3.124s passed
seqConcatWithSeqEmpty2 data()[158] 3.111s passed
seqReverseOfSeqEmpty data()[159] 3.099s passed
div_one data()[15] 3.151s passed
subSeqComplete data()[160] 3.109s passed
subSeqTailR data()[161] 3.130s passed
subSeqTailL data()[162] 3.117s passed
subSeqTailEQR data()[163] 3.125s passed
subSeqTailEQL data()[164] 3.125s passed
seqDef_split data()[165] 3.129s passed
seqDef_induction_upper data()[166] 3.166s passed
seqDef_induction_upper_concrete data()[167] 3.119s passed
seqDef_induction_lower data()[168] 3.147s passed
seqDef_induction_lower_concrete data()[169] 3.169s passed
jdiv_one data()[16] 3.187s passed
seqDef_split_in_three data()[170] 3.244s passed
seqDef_empty data()[171] 3.128s passed
seqDef_one_summand data()[172] 3.127s passed
seqDef_lower_equals_upper data()[173] 3.109s passed
seqDefOfSeq data()[174] 3.166s passed
seqSelfDefinitionEQ2 data()[175] 3.244s passed
indexOfSeqSingleton data()[176] 3.107s passed
indexOfSeqConcatFirst data()[177] 3.123s passed
indexOfSeqConcatSecond data()[178] 3.129s passed
indexOfSeqSub data()[179] 3.132s passed
div_zero data()[17] 3.205s passed
lenOfArray2seq data()[180] 3.112s passed
getAnyOfArray2seq data()[181] 3.097s passed
getOfArray2seq data()[182] 3.109s passed
getAnyOfNPermInv data()[183] 3.112s passed
seqNPermRange data()[184] 3.190s passed
seqPermTrans data()[185] 3.143s passed
seqPermRefl data()[186] 3.115s passed
seqPermSplit data()[187] 3.130s passed
seqNPermRight data()[188] 3.316s passed
seqPermFromSwap data()[189] 3.160s passed
divResZero1 data()[18] 3.188s passed
seqPermTransAlt0 data()[190] 3.102s passed
seqPermTransAlt1 data()[191] 3.131s passed
seqPermTransAlt2 data()[192] 3.096s passed
seqPermTransAlt3 data()[193] 3.105s passed
seqPermForall data()[194] 3.246s passed
seqPermExists data()[195] 3.164s passed
schiffl_lemma_2 data()[196] 21.059s passed
schiffl_thm_1 data()[197] 3.761s passed
eqSameSeq data()[198] 3.357s passed
divResZero2 data()[19] 3.146s passed
eqTermCut data()[1] 3.700s passed
divResOne1 data()[20] 3.186s passed
divResOne2 data()[21] 3.184s passed
div_cancel1 data()[22] 3.178s passed
div_cancel2 data()[23] 3.127s passed
divAddMultDenom data()[24] 3.175s passed
divMinus data()[25] 3.209s passed
divMinusDenom data()[26] 3.167s passed
divLeastDPos data()[27] 3.112s passed
divLeastDNeg data()[28] 3.146s passed
divGreatestDPos data()[29] 3.177s passed
equivAllRight data()[2] 3.494s passed
divGreatestDNeg data()[30] 3.141s passed
divIncreasingPos data()[31] 3.195s passed
divIncreasingNeg data()[32] 3.175s passed
jdiv_zero data()[33] 3.122s passed
jdivPulloutMinusNum data()[34] 3.118s passed
jdivPulloutMinusDenom data()[35] 3.158s passed
jdiv_uniquePosPos data()[36] 3.149s passed
jdiv_uniquePosNeg data()[37] 3.132s passed
jdiv_uniqueNegPos data()[38] 3.125s passed
jdiv_uniqueNegNeg data()[39] 3.165s passed
irrflConcrete1 data()[3] 3.405s passed
jdivMultDenom1 data()[40] 3.175s passed
jdivMultDenom2 data()[41] 3.102s passed
mod_geZero data()[42] 3.113s passed
mod_lessDenom data()[43] 3.110s passed
jmod_NumPos data()[44] 3.115s passed
jmod_NumNeg data()[45] 3.106s passed
jmod_geZero data()[46] 3.095s passed
jmodNumZero data()[47] 3.113s passed
jmod_pulloutminusNum data()[48] 3.103s passed
jmod_pulloutminusDenom data()[49] 3.091s passed
irrflConcrete2 data()[4] 3.341s passed
jmodUnique1 data()[50] 3.212s passed
jmodUnique2 data()[51] 3.151s passed
intDivRem data()[52] 3.085s passed
jmodjmod data()[53] 3.128s passed
jmodDivisible data()[54] 3.139s passed
jmodDivisibleRep data()[55] 3.089s passed
jdivAddMultDenom data()[56] 3.223s passed
jmodAltZero data()[57] 3.126s passed
jmodAddMultDenomZero data()[58] 3.101s passed
polyDiv_zero data()[59] 3.089s passed
cancel_gtPos data()[5] 3.389s passed
polyMod_ltdivDenom data()[60] 3.091s passed
bsum_empty data()[61] 3.100s passed
bsum_induction_upper data()[62] 3.094s passed
bsum_induction_lower data()[63] 3.106s passed
bsum_num_of_bounds data()[64] 3.156s passed
bsum_num_of_bounds2 data()[65] 3.100s passed
bsum_induction_upper2 data()[66] 3.124s passed
bsum_induction_upper_concrete data()[67] 3.109s passed
bsum_induction_upper_concrete_2 data()[68] 3.114s passed
bsum_induction_upper2_concrete data()[69] 3.092s passed
cancel_gtNeg data()[6] 3.252s passed
bsum_induction_lower_concrete data()[70] 3.100s passed
bsum_induction_lower2 data()[71] 3.111s passed
bsum_induction_lower2_concrete data()[72] 3.071s passed
bsum_positive data()[73] 3.137s passed
bsum_upper_bound data()[74] 3.134s passed
bsum_lower_bound data()[75] 3.143s passed
bsum_positive_lower_bound_element data()[76] 3.141s passed
bsum_sub_same_index data()[77] 3.116s passed
bsum_less_same_index data()[78] 3.155s passed
bsum_equal_except_one_index data()[79] 3.110s passed
moduloIntIsInInt data()[7] 3.238s passed
bsum_num_of_is_max data()[80] 3.087s passed
bsum_num_of_is_max2 data()[81] 3.105s passed
bsum_num_of_is_max3 data()[82] 3.151s passed
bsum_num_of_is_max4 data()[83] 3.107s passed
bsum_num_of_lt_max data()[84] 3.090s passed
bsum_num_of_lt_max2 data()[85] 3.126s passed
bsum_num_of_lt_max3 data()[86] 3.112s passed
bsum_num_of_lt_max4 data()[87] 3.095s passed
bsum_num_of_gt0 data()[88] 3.112s passed
bsum_num_of_gt0_alt data()[89] 3.127s passed
moduloLongIsInLong data()[8] 3.169s passed
bsum_add_concrete data()[90] 3.101s passed
bprod_all_positive data()[91] 3.103s passed
bprod_split data()[92] 3.095s passed
powConcrete0 data()[93] 3.088s passed
powConcrete1 data()[94] 3.081s passed
powSplitFactor data()[95] 3.098s passed
powAdd data()[96] 3.117s passed
powMono data()[97] 3.094s passed
powMonoConcrete data()[98] 3.091s passed
powMonoConcreteRight data()[99] 3.079s passed
moduloShortIsInShort data()[9] 3.199s passed

Standard output

604        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
625        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9ms 
849        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
875        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)

1696       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1698       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1700       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1701       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3108       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8138       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.29s 
8199       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8229       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34ns 
8241       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8242       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 589.9ns 
8246       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10966      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
10968      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11910      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11933      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.63ms 
11946      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11946      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 656.5ns 
11948      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14544      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
14545      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15422      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15437      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.93ms 
15440      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15440      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.1ns 
15442      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17980      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
17981      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18825      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18841      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.06ms 
18846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18847      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150ns 
18848      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21360      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
21361      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22180      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22185      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
22188      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22188      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 494.6ns 
22190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24667      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
24668      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25504      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25568      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.57ms 
25577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25578      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 452ns 
25579      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27989      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
27989      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28809      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28827      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.94ms 
28829      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28829      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.1ns 
28830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
31239      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32065      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 702.3ns 
32066      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32067      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.3ns 
32067      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34441      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
34441      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35232      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35235      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 587ns 
35236      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35236      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.1ns 
35237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37636      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
37636      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38433      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 521.6ns 
38435      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38435      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.1ns 
38436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40837      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
40837      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41602      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41604      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 609.5ns 
41606      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41606      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 144.9ns 
41607      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44043      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
44044      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44823      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44826      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 518.8ns 
44829      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44829      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 346.8ns 
44831      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47214      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
47214      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47988      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
48053      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.03ms 
48062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
48062      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.5ns 
48066      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50441      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
50441      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
51221      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
51303      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 73.73ms 
51308      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
51308      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 557ns 
51310      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53731      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
53731      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
54517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54759      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 229.55ms 
54763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54764      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.1ns 
54765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57132      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
57132      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57912      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
57914      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57914      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.3ns 
57915      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60279      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
60281      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
61093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
61099      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
61101      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
61101      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.4ns 
61102      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63510      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
63510      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
64267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
64304      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.1ms 
64307      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
64307      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.9ns 
64308      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66700      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
66701      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
67476      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
67492      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.95ms 
67494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
67494      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.5ns 
67495      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69851      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
69851      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
70625      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
70638      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.53ms 
70639      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
70640      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.3ns 
70640      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73010      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
73011      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
73805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
73823      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.99ms 
73826      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
73826      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.1ns 
73827      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76214      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
76214      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
76985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
77007      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.62ms 
77014      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
77016      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.31ms 
77018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79394      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
79395      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
80166      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
80190      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.04ms 
80191      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
80192      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.8ns 
80192      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82543      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
82543      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
83315      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
83317      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
83319      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
83319      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.4ns 
83320      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85698      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
85701      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
86453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
86492      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.53ms 
86494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
86494      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.5ns 
86495      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88870      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
88871      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
89646      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
89701      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.19ms 
89704      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
89705      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 953ns 
89706      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92059      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
92059      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
92829      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
92869      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.24ms 
92870      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
92870      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.2ns 
92871      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95205      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
95205      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
95973      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
95980      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
95981      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
95982      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 
95982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98352      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
98354      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
99110      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
99126      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.02ms 
99132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
99133      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.2ns 
99134      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
101522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
102295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
102307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ms 
102309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
102309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 
102309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
104650     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
105437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
105447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.66ms 
105451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
105451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.5ns 
105452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
107838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
108624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
108645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.66ms 
108647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
108647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
108648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
111034     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
111814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
111821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.5ms 
111822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
111822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.4ns 
111823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
114168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
114939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
114942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
114943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
114943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
114944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
117282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
118051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
118060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.08ms 
118061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
118062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
118062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
120424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
121171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
121218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.71ms 
121219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
121219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.1ns 
121220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
123582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
124350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
124368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.81ms 
124369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
124369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.3ns 
124370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
126709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
127478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
127499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.13ms 
127502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
127503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.3ns 
127504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
129842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
130609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
130625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.77ms 
130626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
130626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.4ns 
130627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
133002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
133773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
133789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.86ms 
133792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
133792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.3ns 
133793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
136140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
136928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
136965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.87ms 
136967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
136967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
136968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
139300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
140065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
140068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 936.1ns 
140069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
140069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
140070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
142423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
143176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
143180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
143181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
143181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
143182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
145520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
146283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
146290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.16ms 
146292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
146292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns 
146292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
148629     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
149398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
149405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.13ms 
149407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
149407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.1ns 
149408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
151731     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
152494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
152511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.41ms 
152512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
152512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.8ns 
152513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
154853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
155598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
155606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.46ms 
155607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
155607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.7ns 
155608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
157945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
158717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
158720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
158721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
158721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
158722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
161055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
161819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
161823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
161824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
161824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
161825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
164166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
164910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
164913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
164914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
164914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
164915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
167297     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
168062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
168125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.09ms 
168126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
168126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.1ns 
168127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
170448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
171209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
171276     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.76ms 
171277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
171277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 
171278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
173597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
174358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
174361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
174362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
174362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
174363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
176708     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
177460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
177490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.5ms 
177491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
177491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.5ns 
177492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
179839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
180602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
180628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.7ms 
180629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
180630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
180630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
182954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
183715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
183718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 928.5ns 
183719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
183719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
183724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
186070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
186813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
186940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 115.22ms 
186942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
186942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.8ns 
186943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
189294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
190056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
190066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.09ms 
190067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
190067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
190068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
192395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
193160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
193167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.22ms 
193168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
193168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
193169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
195483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
196242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
196256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.62ms 
196258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
196258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
196258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
198590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
199335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
199346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.83ms 
199349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
199349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.6ns 
199350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
201683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
202444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
202447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
202448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
202448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
202449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
204774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
205535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
205539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
205544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
205544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223ns 
205545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
207887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
208627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
208649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.18ms 
208650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
208650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
208651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
211022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
211789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
211804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.33ms 
211806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
211806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
211806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
214129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
214891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
214904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.22ms 
214906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
214906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
214906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
217235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
218025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
218028     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
218030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
218031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.7ns 
218032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
220391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
221133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
221138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
221139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
221139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157ns 
221140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
223483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
224247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
224252     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
224254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
224254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.8ns 
224257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
226579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
227341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
227343     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
227345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
227345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
227345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
229667     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
230441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
230443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.6ns 
230444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
230444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
230445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
232785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
233551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
233555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.02ms 
233556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
233556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
233557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
235865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
236623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
236626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 872.8ns 
236627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
236627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
236628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
238951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
239715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
239762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.48ms 
239764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
239764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185ns 
239765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
242102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
242846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
242896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.05ms 
242899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
242899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.4ns 
242900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
245246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
246007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
246041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.08ms 
246042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
246042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
246043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
248374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
248374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
249136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
249181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.04ms 
249182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
249182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
249183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
251502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
251502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
252267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
252298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.75ms 
252299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
252299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
252300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
254631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
255371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
255452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.56ms 
255454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
255454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
255456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
257774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
258536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
258563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.35ms 
258564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
258564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
258565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
260870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
261630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
261649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.37ms 
261651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
261651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
261651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
263983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
264727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
264754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.26ms 
264756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
264756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.7ns 
264757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
267125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
267886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
267905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.28ms 
267906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
267906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
267907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
270222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
270984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
271012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.66ms 
271013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
271013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
271014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
273320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
274079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
274103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.09ms 
274104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
274104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
274105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
276439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
277204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
277229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.2ms 
277230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
277230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
277231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
279555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
280316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
280340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.85ms 
280341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
280341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
280342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
282655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
283415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
283435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.04ms 
283437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
283437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
283437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
285779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
286524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
286548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.88ms 
286549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
286549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
286550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
288887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
289650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
289674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.92ms 
289676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
289676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.5ns 
289677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
292002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
292769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
292776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.28ms 
292777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
292777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
292778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
295101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
295862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
295879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
295880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
295880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
295880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
298209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
298970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
298973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
298974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
298974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
298975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
301296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
302059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
302061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 533.9ns 
302062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
302062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
302063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
304375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
305141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
305143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.2ns 
305144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
305144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
305145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
307474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
308225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
308239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
308242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
308242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.9ns 
308245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
310585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
311351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
311357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms 
311359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
311359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.5ns 
311360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
313674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
314439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
314451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.77ms 
314452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
314452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
314453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
316778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
317539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
317542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
317543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
317543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
317544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
319875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
320619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
320621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 497.4ns 
320623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
320623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
320623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
322967     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
323729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
323734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.32ms 
323735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
323735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
323736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
326045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
326811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
326813     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 514.7ns 
326814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
326814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
326815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
329147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
329892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
329894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 562.7ns 
329895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
329895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
329896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
332234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
332993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
332995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.8ns 
332996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
332996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
332997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
335316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
336077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
336080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
336081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
336081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
336082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
338401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
339164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
339173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.78ms 
339174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
339175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
339175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
341524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
342270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
342274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
342275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
342275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
342276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
344625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
345418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
345425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.78ms 
345426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
345426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
345427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
347844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
348636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
348640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
348641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
348641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
348642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
351066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
351859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
351874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.61ms 
351876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
351876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
351876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
354315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
355085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
355089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
355090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
355090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
355090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
357533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
358317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
358320     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
358321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
358321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
358322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
360643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
361408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
361411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
361412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
361412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
361413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
363758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
364515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
364532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.21ms 
364533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
364533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
364534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
366880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
367642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
367646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 645.2ns 
367648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
367648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
367649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
369979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
370736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
370773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.27ms 
370774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
370774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
370775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
373115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
373858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
373861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
373863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
373863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.7ns 
373863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
376197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
376969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
376992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.69ms 
376994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
376994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.8ns 
376995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
379325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
380086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
380106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.17ms 
380107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
380107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
380108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
382445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
383192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
383215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.16ms 
383217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
383217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
383217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
385547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
386313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
386316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 549.2ns 
386318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
386318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 643.3ns 
386319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
388635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
389395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
389401     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
389402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
389402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
389402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
391745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
392508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
392511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
392512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
392512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
392513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
394836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
395604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
395607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 744.6ns 
395608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
395608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.3ns 
395609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
397946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
398692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
398694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 850.1ns 
398695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
398695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
398696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
401039     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
401803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
401806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
401807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
401807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.7ns 
401808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
404144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
404891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
404894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
404895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
404895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
404896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
407289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
408076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
408084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.48ms 
408085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
408085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
408086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
410407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
411177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
411188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.42ms 
411191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
411191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 194.2ns 
411192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
413530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
414294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
414304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ms 
414305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
414305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
414306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
416614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
417384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
417396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.51ms 
417397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
417397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
417398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
419772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
420545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
420549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
420550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
420550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
420551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
422925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
423724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
423729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.93ms 
423730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
423730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
423731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
426157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
426947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
426949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 469.9ns 
426950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
426950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 41.6ns 
426951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
429270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
430039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
430042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
430043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
430043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
430043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
432366     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
433133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
433135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 714.5ns 
433136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
433136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
433137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
435466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
436219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
436229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.31ms 
436231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
436232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.8ns 
436232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
438583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
439349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
439353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
439354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
439354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.9ns 
439355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
441688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
442441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
442448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
442449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
442449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
442450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
444780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
445551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
445553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.1ns 
445554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
445554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
445554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
447895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
448691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
448693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.6ns 
448694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
448694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.8ns 
448694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
451077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
451846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
451850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
451852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
451852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 164.4ns 
451852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
454188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
454958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
454960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
454962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
454962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
454963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
457287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
458054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
458057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
458058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
458058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
458059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
460369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
461136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
461138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
461139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
461139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43ns 
461140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
463471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
464242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
464247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.52ms 
464248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
464248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
464249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
466600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
467352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
467355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
467356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
467356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
467357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
469694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
470465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
470476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.19ms 
470478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
470478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 196.3ns 
470479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
472811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
473580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
473582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 639ns 
473583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
473583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
473584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
475918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
476683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
476690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
476691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
476691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
476691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
479019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
479788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
479790     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 842.1ns 
479792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
479792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.2ns 
479793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
482115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
482886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
482888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 748.1ns 
482889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
482889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.3ns 
482890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
485217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
485988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
485993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
485994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
485994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
485994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
488327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
489076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
489079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
489080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
489080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
489081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
491405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
492176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
492179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
492180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
492180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
492181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
494517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
495288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
495292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
495293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
495293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
495294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
497623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
498389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
498394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.14ms 
498395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
498395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
498396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
500728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
501503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
501517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms 
501519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
501519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
501519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
503861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
504613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
504628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.63ms 
504629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
504629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
504630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
506950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
507718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
507728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.93ms 
507729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
507729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
507729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
510058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
510826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
510836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.47ms 
510837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
510838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
510838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
513171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
513941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
513966     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.45ms 
513967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
513967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
513968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
516289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
517060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
517084     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.85ms 
517085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
517085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
517086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
519415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
520186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
520209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.85ms 
520210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
520210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
520211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
522551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
523320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
523333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.66ms 
523334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
523334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
523335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
525657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
526434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
526462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.31ms 
526464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
526464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
526464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
528801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
529555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
529628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.16ms 
529629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
529629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
529630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
531961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
532711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
532747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.04ms 
532749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
532749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
532749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
535103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
535854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
535894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.23ms 
535896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
535896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
535896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
538264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
539020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
539063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.77ms 
539064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
539064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
539065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
541393     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
542164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
542308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 136.58ms 
542309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
542309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
542310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
544652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
545428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
545435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.74ms 
545437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
545437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
545437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
547784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
548555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
548563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
548564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
548564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
548564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
550897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
551666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
551671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.48ms 
551672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
551672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
551673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
554019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
554820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
554838     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.74ms 
554839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
554839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
554840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
557274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
558071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
558082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.55ms 
558083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
558083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
558084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
560415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
561185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
561188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
561190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
561190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
561190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
563520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
564295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
564311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.18ms 
564312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
564312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
564313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
566654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
567424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
567440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.54ms 
567441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
567441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
567442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
569783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
570554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
570572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.63ms 
570573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
570573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
570574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
572908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
573681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
573684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 979.5ns 
573685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
573685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
573686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
576007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
576779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
576782     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
576783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
576783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
576784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
579112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
579884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
579890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.39ms 
579891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
579891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
579892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
582245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
582997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
583003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.33ms 
583004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
583004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.2ns 
583005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
585354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
586125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
586192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.48ms 
586194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
586194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
586194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
588536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
589310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
589336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.68ms 
589337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
589337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
589337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
591661     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
592429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
592451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.37ms 
592452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
592452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
592453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
594804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
595578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
595580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 256.2ns 
595582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
595582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.4ns 
595583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
597929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
598702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
598896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 181.67ms 
598897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
598898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.3ns 
598898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
601233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
602006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
602056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.59ms 
602058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
602058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.3ns 
602059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
604388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
605157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
605159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 325ns 
605160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
605161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
605161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
607519     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
608289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
608291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 330.2ns 
608292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
608292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.6ns 
608292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
610615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
611385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
611387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 303ns 
611388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
611388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.7ns 
611388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
613718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
614490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
614492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 545.5ns 
614493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
614493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
614493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
616828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
617600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
617737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 135.19ms 
617739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
617739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
617739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
620081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
620852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
620902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.66ms 
620903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
620903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
620904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
623245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
624024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
624026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ns 
624050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
624085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
624102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
624107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
624112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
624115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
624116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
624118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
624121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
624122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
624124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
624125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
624343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
624344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
624345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
624347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
624348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
624479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
624480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
624483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
624485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
624486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
624487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
624633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
624636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
624637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
624638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
624638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
624642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
624767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
624769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
624770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
624771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
624772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
624772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
624780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
624780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
624781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
624783     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
624786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
624787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
624795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
624796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
624797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
624797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
624798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
624799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
624915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
624915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
624917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
625046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
625048     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)'' 
625050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
625051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
625052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
625053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
625054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
625056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
625062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
625063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
625064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
625065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
625066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
625155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
625158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
625159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
625160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
625161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
625162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
625163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
625269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
625270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
625271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
625272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
625272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
625273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
625274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
625276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
625370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
625371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
625495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
625498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
625503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
625504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
625505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
625506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
625509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
625509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
625510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
625511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
625518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
625523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
625604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
625605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
625607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
625608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
625609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
625609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
625611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
625612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
625656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
625660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
625734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
625735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
625738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
625739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
625740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
625741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
625855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
625858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
625861     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)'' 
625863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
625864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
625865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
625865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
625866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
625874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
625879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
625881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
625881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
625963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
625964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
625965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
625966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
625967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
625967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
626054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
626056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
626057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
626058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
626059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
626059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
626060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
626061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
626145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
626146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
626215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
626215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
626216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
626220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
626223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
626227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
626335     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
626336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
626337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
626338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
626347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
626419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
629721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
629722     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)'' 
629727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
629728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
629728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
629729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
629729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
629736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
629738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
629739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
629739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
629740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
629828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
629831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
629833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
629833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
629834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
629835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
629835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
629924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
629926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
629927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
629928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
629928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
629929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
629929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
629930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
630003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
630005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
630080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
630084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
630088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
630089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
630089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
630090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
630100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
630177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
630178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
630179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
630180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
630248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
630257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
630257     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)'' 
630259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
630260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
630261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
630261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
630262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
630271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
630273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
630274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
630274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
630275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
630357     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
630359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
630360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
630361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
630361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
630447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
630451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
630453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
630453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
630454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
630454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
630455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
630596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
630598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
630598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
630600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
630600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
630601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
630601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
630602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
630603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
630603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
630604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
630605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
630605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
630605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
630606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
630688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
630689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
630694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
630766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
630841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
630842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
630843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
630843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
630844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
630844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
630845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
630845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
630846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
630926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
630931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
631016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
631017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
631018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
631019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
631019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
631019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
631020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
631020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
631025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
631025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
631100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
631104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
631109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
631202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
631203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
631204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
631205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
631205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
631205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
631206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
631206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
631257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
631258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
631259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
631259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
631260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
631265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
631270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
631378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
631461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
631463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
631463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
631464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
631623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
631705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
631706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
634628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
634633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
634634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
634635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
634635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
634741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
634742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
634743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
634743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
634744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
634841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
637715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
640744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
640749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
640749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
640750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
640751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
640855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
640856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
640857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
640858     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)' ...' 
640860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
641961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
641961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.6ns 
641962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
644338     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
645123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
645125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
645125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
645131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
645141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
645144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
645145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
645146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
645149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
645151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
645153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
645155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
645156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
645163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
645164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
645165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
645259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
645260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
645261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
645262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
645262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
645314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
645315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
645316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
645317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
645317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
645320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
645321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
645321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
645322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
645323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
645324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
645386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
645387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
645387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
645389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
645389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
645390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
645454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
645455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
645455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
645456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
645456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
645457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
645458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
645458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
645459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
645459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
645459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
645460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
645460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
645461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
645461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
645462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
645462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
645463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
645464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
645466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
645496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
645497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
645538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
645539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
645541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
645542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
645542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
645543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
645580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
645582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
645583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
645584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
645585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
645586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
645586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
645624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
645627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
645630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
645675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
645724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
645724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.9ns 
645725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
648171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
649048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
649078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.61ms