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

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

tests
0

failures
0

ignored
10m45.21s

duration
100%

successful

Tests

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

Standard output

392        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
412        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.63ms 
613        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626        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)

1491       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1493       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1494       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1494       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3102       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8479       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.87s 
8539       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8571       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.9ns 
8584       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8586       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.7ms 
8593       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11455      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
11457      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12375      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12406      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.09ms 
12417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12417      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.9ns 
12419      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15048      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.63s 
15048      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15891      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15905      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.91ms 
15907      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15907      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148ns 
15908      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18494      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
18495      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19352      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
19359      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19359      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.61ns 
19360      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21872      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
21872      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22718      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22731      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.33ms 
22737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22738      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 797.82ns 
22740      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25186      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
25187      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25997      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26036      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.92ms 
26040      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26040      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.11ns 
26042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28506      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
28507      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29313      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.28ms 
29319      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29320      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.31ns 
29321      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31801      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
31801      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32592      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32595      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 737.02ns 
32605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32606      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.91ns 
32607      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35068      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
35069      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35844      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.01ns 
35846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35846      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.4ns 
35847      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38266      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
38266      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39061      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39063      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 653.82ns 
39065      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39065      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110ns 
39066      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41451      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
41451      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42242      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 603.71ns 
42245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42246      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.61ns 
42247      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44642      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
44643      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45439      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45442      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 557.81ns 
45445      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45446      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 486.81ns 
45447      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47854      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
47855      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
48638      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
48720      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 78.79ms 
48724      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
48724      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 413.01ns 
48727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51109      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
51109      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
51892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
51924      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.94ms 
51926      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
51926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.3ns 
51927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54290      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
54290      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55073      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55238      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 157.85ms 
55242      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55242      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.9ns 
55243      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57638      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
57639      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
58442      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
58447      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.96ms 
58448      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
58449      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.1ns 
58449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60803      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
60804      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
61586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
61589      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
61591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
61591      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.1ns 
61592      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63969      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
63969      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
64727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
64763      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.26ms 
64765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
64765      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
64766      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67167      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
67167      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
67938      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
67953      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.24ms 
67955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
67955      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.5ns 
67956      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70340      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
70340      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71105      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71124      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.17ms 
71139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71139      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 414.71ns 
71140      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73562      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
73562      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
74346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
74361      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.86ms 
74363      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
74364      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.21ns 
74365      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76768      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
76768      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
77553      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
77567      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.08ms 
77568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
77568      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.4ns 
77569      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79942      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
79943      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
80724      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
80762      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.96ms 
80763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
80763      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.5ns 
80764      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83128      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
83128      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
83902      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
83905      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
83906      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
83906      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.7ns 
83907      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86256      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
86257      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
87032      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
87070      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.03ms 
87071      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
87072      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.7ns 
87073      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89431      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
89431      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
90209      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
90263      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.17ms 
90265      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
90266      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.1ns 
90267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92632      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
92632      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
93410      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
93451      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.72ms 
93453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
93453      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.7ns 
93454      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95811      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
95811      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
96599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
96607      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
96608      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
96609      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.8ns 
96609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98978      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
98978      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
99737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
99750      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.22ms 
99752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
99752      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.5ns 
99753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
102127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
102881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
102891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.57ms 
102893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
102893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.2ns 
102894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
105271     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
106026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
106033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.49ms 
106036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
106036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 316.01ns 
106037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
108424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
109209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
109217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.19ms 
109220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
109220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 581.21ns 
109221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
111580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
112360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
112367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
112368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
112368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
112369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
114737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
115516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
115520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
115522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
115522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.8ns 
115523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
117884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
118660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
118670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.02ms 
118671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
118671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.7ns 
118672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
121016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
121791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
121839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.83ms 
121841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
121841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
121842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
124193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
124968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
124985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.02ms 
124987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
124987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 408.31ns 
124988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
127347     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
128132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
128150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.68ms 
128153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
128153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 289.21ns 
128154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
130513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
131289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
131306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.92ms 
131307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
131307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
131308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
133676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
134428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
134443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.72ms 
134444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
134445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
134445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
136811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
137563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
137602     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.47ms 
137603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
137604     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
137604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
139975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
140727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
140729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
140731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
140731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
140732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
143107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
143884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
143888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
143889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
143889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.8ns 
143890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
146286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
147059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
147067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.77ms 
147069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
147069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.5ns 
147070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
149424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
150218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
150226     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.11ms 
150227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
150227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
150228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
152578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
153351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
153369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.22ms 
153370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
153371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131ns 
153371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
155707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
156479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
156487     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.94ms 
156488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
156488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
156489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
158833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
159625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
159628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
159631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
159631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.2ns 
159632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
161985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
162759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
162762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
162764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
162764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
162764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
165106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
165884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
165888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
165889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
165889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.4ns 
165890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
168237     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
169011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
169081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.88ms 
169083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
169083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.4ns 
169084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
171449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
172203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
172288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 77.06ms 
172290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
172290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.9ns 
172291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
174663     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
175412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
175415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
175416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
175416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
175417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
177781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
178554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
178594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.63ms 
178596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
178597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 417.1ns 
178598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
180943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
181715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
181745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.46ms 
181747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
181747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.9ns 
181748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
184090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
184864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
184867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
184868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
184868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
184870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
187206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
187977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
188140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 152.85ms 
188142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
188142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
188143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
190494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
191270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
191282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.17ms 
191283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
191283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
191284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
193625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
194404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
194420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.17ms 
194421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
194421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
194422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
196757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
197531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
197547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.83ms 
197549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
197549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
197549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
199906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
200654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
200666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.31ms 
200668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
200668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
200669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
203027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
203776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
203780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
203781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
203781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
203782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
206136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
206883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
206888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
206889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
206889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
206890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
209249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
209999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
210022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.57ms 
210023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
210023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
210024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
212395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
213172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
213188     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.51ms 
213190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
213190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
213191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
215541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
216325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
216340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.71ms 
216341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
216341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.6ns 
216342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
218692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
219465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
219469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
219470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
219470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
219471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
221824     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
222600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
222604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.82ms 
222606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
222606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
222606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
224963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
225736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
225742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
225743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
225743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
225744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
228079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
228853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
228857     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
228859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
228859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.4ns 
228860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
231205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
231975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
231977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.41ns 
231979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
231979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
231979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
234315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
235086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
235089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
235090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
235091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
235091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
237463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
238211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
238214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
238215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
238215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
238216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
240579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
241329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
241391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.52ms 
241393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
241393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
241393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
243763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
244514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
244549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.64ms 
244550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
244550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
244551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
246921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
247692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
247723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.16ms 
247724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
247724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
247725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
250076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
250849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
250892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.34ms 
250894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
250894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
250895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
253244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
254016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
254049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.51ms 
254050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
254050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
254051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
256403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
257176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
257230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.8ms 
257231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
257231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
257232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
259588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
260363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
260390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.59ms 
260392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
260392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
260393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
262758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
263532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
263555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18ms 
263557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
263557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.6ns 
263558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
265917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
266689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
266713     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.43ms 
266715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
266715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
266716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
269081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
269832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
269852     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.58ms 
269854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
269854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
269855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
272218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
272966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
272994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.96ms 
272995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
272995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
272996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
275359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
276106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
276131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.06ms 
276132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
276132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
276133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
278493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
279269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
279294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.06ms 
279295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
279295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
279296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
281649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
282418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
282443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.64ms 
282444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
282444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
282445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
284785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
285558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
285579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.46ms 
285581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
285581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
285582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
287921     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
288692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
288716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.89ms 
288717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
288717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
288718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
291055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
291826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
291850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.36ms 
291851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
291851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
291852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
294180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
294951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
294958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms 
294959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
294960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
294960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
297306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
298077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
298094     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.66ms 
298095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
298095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
298096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
300438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
301210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
301214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
301215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
301215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
301216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
303571     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
304323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
304325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 611.41ns 
304326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
304327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
304327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
306686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
307438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
307441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 713.91ns 
307442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
307442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
307443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
309804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
310557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
310564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
310565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
310565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
310566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
312928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
313709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
313715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.05ms 
313717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
313717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
313717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
316060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
316834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
316846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.57ms 
316847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
316847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
316848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
319191     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
319969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
319973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
319974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
319974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
319975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
322321     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
323093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
323095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 593.21ns 
323097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
323097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
323097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
325436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
326210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
326216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.65ms 
326217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
326217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
326217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
328552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
329330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
329332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 595.11ns 
329333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
329333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
329334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
331664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
332435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
332437     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 560.71ns 
332438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
332439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
332439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
334768     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
335539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
335541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 605.71ns 
335542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
335543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
335543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
337874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
338644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
338648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
338649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
338649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
338649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
340998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
341746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
341754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.69ms 
341755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
341756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
341756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
344109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
344861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
344865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
344867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
344867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
344867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
347222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
347972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
347979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.87ms 
347980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
347980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
347981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
350336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
351106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
351110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
351112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
351112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
351112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
353447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
354218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
354233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.63ms 
354235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
354235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
354236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
356585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
357356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
357360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
357361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
357361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
357362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
359698     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
360473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
360476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
360477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
360477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
360478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
362811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
363580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
363583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
363585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
363585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
363585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
365910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
366684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
366701     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.33ms 
366702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
366702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
366703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
369041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
369814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
369818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 496.81ns 
369821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
369821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.7ns 
369822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
372157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
372925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
372963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.6ms 
372964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
372965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
372965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
375328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
376077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
376080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
376081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
376081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
376082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
378442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
379190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
379211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.19ms 
379212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
379212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
379213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
381572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
382320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
382340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.65ms 
382341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
382341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
382342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
384697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
385468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
385492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.55ms 
385493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
385493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
385494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
387821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
388594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
388596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 530.32ns 
388597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
388597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
388598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
390929     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
391698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
391703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.62ms 
391704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
391704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
391705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
394035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
394816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
394819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
394820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
394820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
394821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
397156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
397932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
397934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 773.02ns 
397935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
397935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
397936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
400267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
401041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
401044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 829.11ns 
401046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
401046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.6ns 
401047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
403402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
404155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
404159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
404160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
404160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
404160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
406510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
407263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
407265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
407267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
407267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
407268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
409620     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
410398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
410407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.04ms 
410408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
410408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
410409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
412736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
413513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
413525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.91ms 
413530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
413531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 595.81ns 
413531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
415867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
416641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
416652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.87ms 
416653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
416653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
416654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
418983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
419768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
419780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.61ms 
419781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
419782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.3ns 
419782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
422135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
422897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
422902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
422903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
422903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
422904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
425254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
426043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
426049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
426050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
426050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
426051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
428381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
429166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
429168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 708.71ns 
429169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
429169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
429170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
431511     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
432299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
432303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
432305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
432305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
432305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
434658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
435447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
435449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 789.42ns 
435451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
435451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
435451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
437801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
438561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
438571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.54ms 
438572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
438572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
438573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
440924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
441707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
441711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
441712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
441712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
441713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
444051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
444837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
444844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
444845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
444845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
444846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
447217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
448004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
448006     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.32ns 
448008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
448008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
448009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
450362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
451122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
451124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.61ns 
451126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
451126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
451126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
453477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
454261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
454265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
454266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
454266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
454267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
456595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
457379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
457382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
457383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
457383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
457383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
459739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
460500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
460503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
460504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
460504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
460505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
462854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
463639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
463642     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
463643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
463643     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
463644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
465980     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
466763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
466772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.18ms 
466773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
466773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
466774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
469128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
469888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
469891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
469892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
469892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
469893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
472246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
473031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
473042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.77ms 
473043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
473043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
473044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
475382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
476164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
476166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 685.61ns 
476167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
476167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
476168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
478512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
479274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
479281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms 
479283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
479283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
479284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
481631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
482414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
482417     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 934.02ns 
482418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
482418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
482419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
484751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
485535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
485537     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 772.41ns 
485538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
485538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
485539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
487889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
488676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
488681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.17ms 
488683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
488683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.3ns 
488683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
491038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
491828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
491831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
491832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
491832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
491833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
494188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
494950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
494953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
494955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
494955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
494955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
497302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
498085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
498089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
498090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
498090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
498091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
500432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
501213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
501217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.11ms 
501219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
501219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
501220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
503567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
504351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
504365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ms 
504367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
504367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
504367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
506705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
507493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
507512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.4ms 
507513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
507513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
507514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
509875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
510659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
510669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.64ms 
510671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
510671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.9ns 
510672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
513031     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
513815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
513826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.94ms 
513827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
513827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
513828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
516181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
516967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
516992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.5ms 
516993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
516994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
516994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
519330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
520117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
520143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.59ms 
520144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
520144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
520145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
522506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
523293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
523316     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.7ms 
523318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
523318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
523318     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.34s 
525658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
526446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
526461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.57ms 
526462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
526462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
526463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
528834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
529623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
529653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.84ms 
529654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
529654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
529655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
531991     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
532776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
532822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.57ms 
532824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
532824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
532824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
535205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
535998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
536036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.49ms 
536038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
536038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
536038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
538415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
539180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
539221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.13ms 
539223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
539223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
539224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
541581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
542368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
542412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.08ms 
542414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
542414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
542415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
544773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
545558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
545681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.11ms 
545683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
545683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
545683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
548027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
548815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
548826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.89ms 
548829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
548829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.7ns 
548829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
551194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
551981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
551989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
551990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
551990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
551991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
554359     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
555145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
555150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
555151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
555151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.7ns 
555152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
557487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
558275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
558292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.77ms 
558293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
558293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
558294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
560652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
561437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
561448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.89ms 
561449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
561449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
561449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
563804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
564593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
564597     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
564598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
564598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
564598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
566937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
567722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
567739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.53ms 
567740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
567740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
567740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
570102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
570888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
570904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.91ms 
570905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
570905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
570906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
573268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
574059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
574079     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.8ms 
574080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
574080     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
574081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
576414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
577198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
577201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
577202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
577202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
577203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
579547     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
580332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
580335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
580336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
580336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
580337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
582680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
583466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
583472     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
583473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
583474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.9ns 
583474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
585821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
586584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
586590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
586591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
586592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
586592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
588936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
589722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
589791     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 64.24ms 
589793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
589793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
589793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
592163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
592949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
592976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.31ms 
592977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
592977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
592978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
595345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
596131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
596152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.8ms 
596154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
596154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
596154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
598508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
599294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
599296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 297ns 
599298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
599298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.6ns 
599300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
601658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
602421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
602649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 218.15ms 
602652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
602652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.8ns 
602653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
605011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
605775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
605825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.98ms 
605827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
605827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
605827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
608176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
608961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
608963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 340.4ns 
608965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
608965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
608965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
611336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
612126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
612128     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 364.4ns 
612130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
612130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
612130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
614483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
615271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
615273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 353.2ns 
615275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
615275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.3ns 
615275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
617618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
618403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
618405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 484.41ns 
618406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
618406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
618407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
620763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
621548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
621655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 105.2ms 
621658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
621658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.6ns 
621659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
624032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
624819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
624877     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.59ms 
624879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
624879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
624880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
627269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
628056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
628058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ns 
628085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
628120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
628137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
628142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
628148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
628151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
628152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
628154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
628157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
628159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
628161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
628162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
628342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
628344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
628345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
628346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
628347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
628487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
628488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
628491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
628493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
628495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
628495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
628673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
628675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
628676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
628677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
628678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
628678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
628818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
628820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
628821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
628822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
628823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
628824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
628831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
628832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
628833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
628835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
628836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
628836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
628844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
628845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
628846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
628847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
628848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
628849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
628987     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
628988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
628990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
629114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
629116     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)'' 
629119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
629120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
629121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
629122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
629123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
629126     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
629130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
629131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
629132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
629133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
629135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
629247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
629251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
629253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
629254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
629255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
629256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
629258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
629375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
629377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
629378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
629380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
629380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
629381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
629383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
629384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
629471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
629472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
629599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
629607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
629616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
629617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
629619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
629620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
629621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
629622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
629624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
629625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
629637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
629642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
629735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
629737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
629738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
629742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
629742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
629743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
629743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
629744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
629796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
629803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
629896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
629898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
629901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
629902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
629904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
629904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
630029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
630033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
630035     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)'' 
630037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
630039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
630040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
630040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
630041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
630050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
630055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
630057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
630060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
630152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
630154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
630155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
630156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
630157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
630158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
630285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
630287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
630288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
630289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
630290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
630291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
630291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
630292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
630376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
630378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
630465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
630465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
630466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
630470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
630474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
630477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
630593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
630595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
630595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
630596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
630605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
630686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
634187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
634188     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)'' 
634193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
634194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
634195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
634195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
634196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
634203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
634204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
634205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
634206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
634206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
634295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
634298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
634299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
634300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
634301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
634301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
634302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
634394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
634395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
634396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
634397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
634397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
634398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
634398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
634399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
634471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
634473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
634543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
634547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
634551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
634552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
634553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
634554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
634563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
634641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
634645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
634645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
634646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
634716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
634724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
634725     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)'' 
634727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
634728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
634728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
634729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
634729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
634739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
634740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
634741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
634742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
634742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
634826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
634827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
634828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
634829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
634830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
634916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
634921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
634922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
634922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
634923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
634923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
634924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
635060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
635061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
635062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
635063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
635064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
635064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
635065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
635066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
635067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
635068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
635069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
635070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
635070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
635071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
635072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
635155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
635156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
635162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
635236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
635313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
635314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
635315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
635316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
635317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
635317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
635317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
635318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
635319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
635400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
635406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
635492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
635493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
635493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
635494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
635495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
635495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
635495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
635496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
635501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
635501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
635579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
635584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
635589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
635685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
635686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
635686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
635687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
635688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
635688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
635688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
635689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
635742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
635743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
635744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
635744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
635745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
635750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
635755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
635866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
635951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
635952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
635952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
635953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
636115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
636200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
636200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
639154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
639159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
639160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
639161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
639161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
639270     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
639272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
639273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
639273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
639274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
639375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
642299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
645353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
645358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
645359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
645360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
645361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
645470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
645471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
645472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
645473     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)' ...' 
645474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
646592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
646592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 157.9ns 
646593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
649015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
649825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
649827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
649827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
649833     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
649844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
649847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
649849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
649849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
649853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
649855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
649857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
649860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
649860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
649868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
649870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
649870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
649917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
649918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
649919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
649919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
649920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
649982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
649983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
649984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
649985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
649985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
649989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
649989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
649990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
649991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
649991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
649992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
650073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
650074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
650074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
650075     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
650076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
650077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
650164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
650165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
650166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
650166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
650167     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
650168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
650168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
650169     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
650170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
650170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
650170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
650171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
650172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
650172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
650173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
650173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
650174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
650175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
650176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
650178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
650218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
650219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
650281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
650283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
650284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
650285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
650286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
650287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
650342     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
650345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
650346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
650348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
650349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
650350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
650350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
650407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
650410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
650413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
650558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
650620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
650620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.2ns 
650621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
652955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
653768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
653801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.05ms