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

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

tests
0

failures
0

ignored
10m40.02s

duration
100%

successful

Tests

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

Standard output

515        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
538        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.07ms 
763        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
776        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)

1742       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1745       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1749       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1750       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3259       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8493       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.73s 
8554       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8584       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.2ns 
8596       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8597       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.8ns 
8601       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11324      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
11326      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12269      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12298      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.57ms 
12312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.5ns 
12313      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14949      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
14954      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15778      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15791      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.33ms 
15794      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15794      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.4ns 
15795      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18322      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
18322      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19159      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.81ms 
19164      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19165      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.6ns 
19166      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21626      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
21626      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22479      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.4ms 
22483      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22484      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 706.7ns 
22485      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24920      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
24920      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25739      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25779      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.21ms 
25781      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.7ns 
25782      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28167      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
28168      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28968      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28994      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.39ms 
28998      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28999      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.4ns 
29000      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31393      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
31393      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32158      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32161      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 620ns 
32163      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32163      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.2ns 
32164      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34552      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
34552      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35344      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 622.4ns 
35345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35346      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.7ns 
35346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37708      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
37708      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38480      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38482      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 531.7ns 
38484      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38484      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.8ns 
38485      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40862      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
40862      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41613      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41616      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 622.2ns 
41617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41617      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
41618      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43998      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
43999      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44771      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 530.5ns 
44774      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44774      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.1ns 
44775      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47137      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
47138      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47924      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47966      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.09ms 
47970      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47971      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.2ns 
47985      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50458      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
50458      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
51226      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
51261      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.99ms 
51263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
51263      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.7ns 
51264      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53617      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
53618      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
54386      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54606      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 209.78ms 
54617      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54617      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.9ns 
54618      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
57026      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
57026      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57798      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57804      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.03ms 
57806      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57806      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307ns 
57807      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60207      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
60208      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60986      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
60989      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60990      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 544.2ns 
60991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63342      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
63342      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
64112      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
64150      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.23ms 
64152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
64152      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.6ns 
64153      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66546      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
66546      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
67317      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
67332      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.05ms 
67334      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
67334      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.5ns 
67335      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69680      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
69680      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
70452      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
70465      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.97ms 
70467      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
70467      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.7ns 
70468      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72856      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
72857      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
73615      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
73631      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.84ms 
73634      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
73634      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.8ns 
73635      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75997      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
75998      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
76773      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
76788      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.57ms 
76790      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
76790      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.4ns 
76791      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79145      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
79145      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
79917      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
79941      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.99ms 
79943      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
79943      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.6ns 
79944      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82317      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
82317      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
83079      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
83083      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
83091      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
83091      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 478.2ns 
83093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85461      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
85462      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
86231      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
86272      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.39ms 
86274      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
86274      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 120.3ns 
86275      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88659      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
88659      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
89426      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
89485      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.16ms 
89488      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
89489      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.3ns 
89490      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91903      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
91903      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
92666      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
92712      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.68ms 
92713      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
92713      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 
92715      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95085      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
95085      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
95853      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
95861      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
95862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
95862      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.6ns 
95863      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98251      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
98251      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
99003      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
99021      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.33ms 
99028      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
99029      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 400.5ns 
99030      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
101409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
102178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
102194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.25ms 
102198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
102198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.9ns 
102199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
104544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
105309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
105317     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
105319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
105319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 291.9ns 
105320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
107678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
108438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
108446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
108448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
108448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.6ns 
108449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
110787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
111549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
111556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.75ms 
111557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
111558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100ns 
111558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
113892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
114652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
114655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
114656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
114656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
114657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
117002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
117770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
117780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ms 
117782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
117782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.8ns 
117784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
120118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
120879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
120929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.04ms 
120932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
120932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.6ns 
120933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
123290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
124035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
124054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.16ms 
124055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
124055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
124056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
126402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
127172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
127199     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.42ms 
127201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
127202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106ns 
127203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
129534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
130305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
130322     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.71ms 
130323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
130323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114ns 
130324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
132665     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
133423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
133440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.17ms 
133441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
133442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
133442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
135771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
136534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
136575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.03ms 
136577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
136577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
136578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
138933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
139670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
139673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
139674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
139674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
139675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
142010     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
142767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
142771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ms 
142772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
142772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81ns 
142773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
145097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
145853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
145861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.62ms 
145862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
145862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
145863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
148200     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
148938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
148946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.87ms 
148947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
148947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
148948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
151284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
152040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
152059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.38ms 
152061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
152061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
152062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
154374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
155134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
155142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
155145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
155145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 268.4ns 
155146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
157488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
158391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
158395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
158399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
158400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.8ns 
158401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160742     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
160742     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
161509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
161512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
161514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
161514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.2ns 
161514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
163863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
164602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
164605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
164607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
164607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
164608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
166947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
167710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
167807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.42ms 
167809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
167810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.7ns 
167811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
170128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
170890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
170969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.77ms 
170971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
170971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.1ns 
170972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
173323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
174079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
174083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
174084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
174084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.7ns 
174085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
176407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
177164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
177212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.48ms 
177214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
177214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.5ns 
177215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
179569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
180308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
180336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.72ms 
180337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
180337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
180338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
182681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
182681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
183438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
183440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
183441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
183441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
183443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
185756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
185756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
186511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
186648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 124ms 
186650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
186650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.5ns 
186650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
189008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
189778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
189789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.68ms 
189791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
189791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.2ns 
189792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
192105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
192864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
192882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.53ms 
192885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
192885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.7ns 
192886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
195211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
195972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
195988     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.5ms 
195990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
195990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
195990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
198331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
199087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
199100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.59ms 
199102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
199103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228ns 
199104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
201424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
202179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
202183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
202184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
202184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
202185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
204537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
205278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
205282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.88ms 
205283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
205283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
205284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
207627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
208388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
208411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.13ms 
208412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
208413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
208413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
210739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
211498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
211515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.39ms 
211516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
211516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
211517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
213858     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
214612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
214627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.43ms 
214628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
214628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
214629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
216937     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
217692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
217695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
217696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
217696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
217697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
220022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
220759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
220763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
220765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
220765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.8ns 
220766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
223091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
223844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
223849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.48ms 
223851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
223851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
223851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
226153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
226908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
226911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
226912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
226912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
226913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
229241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
229976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
229978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 629.7ns 
229979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
229979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
229980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
232302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
233057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
233061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
233062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
233062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
233063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
235379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
236140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
236143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 979.7ns 
236145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
236145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 190.5ns 
236146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
238478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
239233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
239277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.51ms 
239278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
239278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
239283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
241614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
242370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
242403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.32ms 
242404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
242404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
242405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
244748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
245484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
245514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.93ms 
245516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
245516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
245516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
247862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
248621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
248661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.9ms 
248663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
248663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
248664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
250971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
251726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
251754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.08ms 
251755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
251755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
251756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
254080     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
254814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
254886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.37ms 
254887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
254887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
254888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
257190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
257947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
257974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.64ms 
257975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
257975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
257976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
260307     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
261041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
261061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.84ms 
261062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
261062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
261063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
263389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
264145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
264169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.67ms 
264170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
264170     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
264171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
266482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
267240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
267260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.3ms 
267262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
267262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 230.4ns 
267263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
269605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
270346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
270377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27ms 
270378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
270378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
270379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
272726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
273488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
273513     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.27ms 
273516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
273516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 218ns 
273517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
275841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
276602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
276627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.8ms 
276629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
276629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
276630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
278972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
279730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
279754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.45ms 
279755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
279755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
279756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
282069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
282825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
282845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ms 
282846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
282847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
282847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
285174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
285174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
285909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
285934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.14ms 
285935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
285935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
285935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
288263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
289017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
289041     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.31ms 
289042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
289042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
289043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
291348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
292103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
292110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.16ms 
292111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
292111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
292112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
294444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
295202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
295220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.49ms 
295221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
295221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
295222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
297537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
298294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
298298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
298299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
298299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
298299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
300624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
301363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
301365     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 596.9ns 
301366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
301366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
301367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
303694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
304454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
304456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 698.1ns 
304457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
304457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
304458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
306786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
307544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
307551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
307552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
307552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
307552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
309880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
310617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
310623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.04ms 
310625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
310625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.7ns 
310626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
312963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
313723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
313735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.47ms 
313737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
313737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192ns 
313738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
316048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
316809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
316812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
316813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
316813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
316814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
319169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
319926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
319928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 530.4ns 
319929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
319929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
319930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
322247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
323003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
323009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.67ms 
323010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
323010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
323010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
325340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
326078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
326080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 655.3ns 
326081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
326081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
326082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
328413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
329169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
329171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 536.3ns 
329172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
329173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
329173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
331538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
332296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
332298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 604.1ns 
332299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
332300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.3ns 
332300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
334647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
335387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
335390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
335391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
335391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
335392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
337722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
338482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
338492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.47ms 
338493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
338493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
338494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
340810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
341566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
341570     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
341571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
341571     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
341572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343910     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
343910     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
344666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
344673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.86ms 
344674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
344674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
344675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
346986     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
347750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
347754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
347755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
347755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
347756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
350083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
350821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
350836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.31ms 
350837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
350837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
350838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
353164     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
353923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
353926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
353927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
353927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
353928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
356257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
356995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
356998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
356999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
356999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
357000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
359337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
360094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
360098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
360099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
360099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
360100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
362412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
363172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
363190     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.83ms 
363191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
363191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
363191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
365530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
366289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
366294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 560.1ns 
366296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
366297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.8ns 
366297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
368611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
369380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
369420     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.95ms 
369421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
369421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
369422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
371763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
372520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
372523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
372524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
372524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
372525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
374838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
375597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
375618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.17ms 
375619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
375619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
375620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
377954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
378712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
378732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.02ms 
378733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
378733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
378734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
381065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
381804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
381827     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.07ms 
381828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
381828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
381829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
384166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
384925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
384928     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 531.4ns 
384929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
384929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
384929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
387262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
388003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
388008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
388009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
388010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
388010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
390339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
391100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
391103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
391104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
391104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
391105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
393442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
394203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
394206     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 695ns 
394207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
394208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.8ns 
394208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
396527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
397288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
397291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 773.7ns 
397293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
397293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
397294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
399635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
399635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
400396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
400399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
400400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
400401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
400401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
402733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
403476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
403479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
403480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
403480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
403481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
405815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
406575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
406585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.26ms 
406586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
406586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
406587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
408922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
408922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
409683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
409695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.48ms 
409696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
409696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
409697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
412008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
412772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
412783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.33ms 
412785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
412785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44ns 
412785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
415158     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
415925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
415945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.6ms 
415947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
415947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.8ns 
415948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
418282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
419048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
419053     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.55ms 
419055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
419055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.2ns 
419056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
421395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
422142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
422148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.03ms 
422149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
422149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
422150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
424504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
425270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
425272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 649.2ns 
425274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
425274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.9ns 
425274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
427618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
428384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
428387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
428388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
428388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
428389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
430740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
431490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
431493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 786.71ns 
431494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
431494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
431494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
433847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
433847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
434614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
434624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.26ms 
434625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
434625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
434626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
436992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
437757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
437761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
437762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
437762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
437763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
440098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
440864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
440871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.52ms 
440872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
440872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
440872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
443211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
443988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
443991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 659.01ns 
443992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
443992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
443993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
446312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
447079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
447081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 605.9ns 
447082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
447082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
447082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
449418     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
450188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
450192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
450193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
450193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
450194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
452526     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
453291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
453294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
453295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
453295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
453296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
455625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
456389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
456392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
456393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
456394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
456394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
458723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
459487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
459490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
459491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
459491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
459491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
461817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
462562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
462568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.57ms 
462569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
462569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.4ns 
462569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
464889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
465651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
465654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
465655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
465655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
465656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
467994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
467994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
468759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
468769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.23ms 
468770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
468770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
468771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
471089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
471857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
471859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 627.3ns 
471861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
471861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.4ns 
471861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
474186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
474950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
474957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
474958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
474958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
474959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
477280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
478046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
478048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 832.71ns 
478050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
478050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
478051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
480376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
481140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
481142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 750.8ns 
481143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
481143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
481144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
483477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
484242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
484247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
484248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
484248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
484249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
486573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
487350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
487353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
487354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
487354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
487355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
489674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
490436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
490440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
490441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
490441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
490441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
492755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
493521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
493526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
493527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
493527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
493528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
495873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
496639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
496644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.04ms 
496645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
496645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
496646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
498981     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
499747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
499763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.18ms 
499764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
499764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
499764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
502081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
502844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
502859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.06ms 
502860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
502860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
502861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
505178     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
505941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
505950     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.16ms 
505952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
505952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
505952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
508269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
509033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
509045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.49ms 
509046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
509046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
509047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
511371     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
512134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
512159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.22ms 
512160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
512160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
512161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
514478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
515241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
515266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.07ms 
515267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
515267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
515268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
517596     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
518362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
518385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.86ms 
518386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
518386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
518387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
520709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
521477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
521492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.22ms 
521493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
521493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
521494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
523821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
524584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
524615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.4ms 
524616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
524616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
524617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
526954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
527743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
527789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.74ms 
527790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
527790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
527791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
530106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
530869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
530906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.11ms 
530907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
530907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
530907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
533235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
534005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
534046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.81ms 
534047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
534047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
534048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
536383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
537152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
537195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.24ms 
537196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
537196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
537197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
539532     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
540298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
540456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 149.64ms 
540457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
540457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
540458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
542796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
543563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
543571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.71ms 
543573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
543573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
543573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
545918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
546696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
546704     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6ms 
546705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
546705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
546706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
549059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
549824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
549829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
549830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
549830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
549830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
552162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
552926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
552943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.21ms 
552944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
552944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
552945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
555262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
556025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
556036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.55ms 
556037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
556037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
556038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
558362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
559127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
559130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
559131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
559131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
559132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
561443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
562207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
562224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.52ms 
562225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
562225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
562226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
564560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
565325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
565341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.45ms 
565342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
565342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
565342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
567664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
568432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
568452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.87ms 
568454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
568454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.2ns 
568455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
570816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
571586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
571590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
571592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
571592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 176.5ns 
571593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
573922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
574691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
574694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
574696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
574696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
574696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
577024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
577793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
577799     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
577800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
577800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48ns 
577801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
580144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
580910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
580916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.19ms 
580917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
580917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
580918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
583236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
584004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
584071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.91ms 
584073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
584073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
584074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
586488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
587255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
587283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.31ms 
587286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
587286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.2ns 
587287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
589623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
590386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
590407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.9ms 
590408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
590409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
590409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
592745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
593508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
593510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 264ns 
593512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
593512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 168.5ns 
593513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
595838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
596601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
596792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 177.83ms 
596793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
596793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
596794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
599149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
599920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
599969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.25ms 
599970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
599970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
599970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
602286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
603057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
603060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 327.4ns 
603061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
603061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
603061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
605398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
606164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
606166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 316.1ns 
606167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
606167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
606168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
608506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
609268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
609269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 316.5ns 
609271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
609271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
609271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
611583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
612346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
612348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 420.5ns 
612349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
612349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
612349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
614677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
615439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
615533     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
615551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.03ms 
615553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
615553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.7ns 
615555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
617886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
618653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
618702     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
618703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.85ms 
618704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
618704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241ns 
618706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
621052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
621816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
621818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ns 
621841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
621873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
621889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
621893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
621898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
621900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
621901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
621902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
621905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
621907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
621909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
621910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
622116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
622117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
622118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
622119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
622120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
622267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
622268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
622271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
622273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
622274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
622275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
622444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
622446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
622447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
622448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
622449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
622452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
622577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
622578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
622579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
622580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
622582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
622583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
622590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
622591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
622591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
622593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
622595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
622596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
622604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
622605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
622606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
622607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
622607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
622608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
622746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
622746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
622748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
622870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
622871     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)'' 
622874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
622875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
622876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
622877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
622878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
622880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
622884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
622885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
622886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
622887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
622887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
622999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
623002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
623004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
623005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
623005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
623006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
623008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
623175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
623177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
623177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
623179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
623179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
623180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
623180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
623182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
623295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
623297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
623397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
623402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
623406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
623407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
623408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
623409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
623410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
623410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
623411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
623412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
623420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
623424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
623524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
623525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
623526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
623527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
623528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
623528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
623529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
623530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
623582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
623588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
623686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
623688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
623689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
623691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
623692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
623692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
623873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
623878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
623879     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)'' 
623880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
623881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
623882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
623882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
623883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
623892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
623893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
623894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
623895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
624001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
624002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
624003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
624003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
624004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
624005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
624130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
624131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
624132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
624133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
624133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
624134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
624134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
624135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
624218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
624219     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
624292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
624292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
624293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
624297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
624301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
624305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
624422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
624423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
624423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
624424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
624434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
624516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
628059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
628061     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)'' 
628066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
628067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
628068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
628068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
628069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
628076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
628078     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
628080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
628080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
628081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
628171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
628175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
628176     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
628177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
628177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
628178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
628179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
628272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
628274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
628275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
628276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
628276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
628277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
628278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
628279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
628353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
628354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
628426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
628431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
628435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
628436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
628436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
628437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
628447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
628524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
628525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
628526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
628527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
628597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
628606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
628607     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)'' 
628609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
628610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
628611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
628611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
628612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
628622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
628623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
628624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
628625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
628626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
628789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
628797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
628799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
628800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
628801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
628992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
628998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
629000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
629000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
629001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
629002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
629003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
629177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
629179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
629181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
629183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
629183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
629184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
629185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
629186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
629187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
629188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
629189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
629190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
629191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
629191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
629192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
629288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
629289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
629295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
629437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
629532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
629534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
629535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
629536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
629537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
629537     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
629544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
629551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
629552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
629658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
629664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
629752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
629756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
629757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
629765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
629765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
629766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
629766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
629767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
629772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
629772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
629866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
629871     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
629876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
629976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
629977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
629988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
629989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
629990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
629990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
629990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
629991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
630053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
630054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
630054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
630055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
630056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
630061     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
630066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
630198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
630284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
630285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
630286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
630287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
630452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
630539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
630540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
633674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
633679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
633681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
633681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
633687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
633802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
633803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
633805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
633805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
633806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
633912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
636976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
640197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
640202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
640203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
640204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
640204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
640316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
640317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
640318     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
640319     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)' ...' 
640321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
641476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
641476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
641477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
643880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
643880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
644710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
644711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ns 
644712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
644720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
644731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
644734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
644735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
644736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
644740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
644742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
644745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
644748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
644748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
644758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
644759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
644760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
644807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
644808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
644809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
644809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
644810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
644867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
644868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
644869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
644870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
644870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
644874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
644874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
644875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
644876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
644877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
644877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
644952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
644953     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
644954     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
644955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
644956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
644957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
645038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
645039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
645039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
645040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
645041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
645042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
645042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
645042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
645043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
645044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
645044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
645045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
645045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
645046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
645046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
645047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
645047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
645048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
645049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
645051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
645087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
645088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
645138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
645139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
645140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
645142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
645142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
645143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
645186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
645188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
645189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
645190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
645192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
645192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
645193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
645237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
645239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
645242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
645297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
645355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
645355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.7ns 
645356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
647792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
648603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
648634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.09ms