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

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

tests
0

failures
0

ignored
10m37.00s

duration
100%

successful

Tests

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

Standard output

560        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
582        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.36ms 
775        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
787        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)

1730       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1732       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1735       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1735       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3279       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8380       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.6s 
8452       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8484       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.4ns 
8496       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8497       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 483.1ns 
8500       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11243      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
11246      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12201      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12230      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.62ms 
12242      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12242      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.4ns 
12243      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14922      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
14927      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15754      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15767      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.33ms 
15770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15771      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.2ns 
15772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18372      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
18372      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19197      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19212      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.06ms 
19217      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19217      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 142.7ns 
19219      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21635      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
21636      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22441      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22451      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.48ms 
22453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22454      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.36ms 
22455      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24886      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
24886      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25717      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 71.13ms 
25725      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25726      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 619.1ns 
25727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28148      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
28149      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28926      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28943      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.37ms 
28946      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28947      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.5ns 
28948      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31314      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
31315      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32089      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32093      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 686.9ns 
32095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32096      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 366.6ns 
32097      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34481      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
34481      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35267      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35275      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 564.7ns 
35277      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35278      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 445.2ns 
35279      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37654      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
37655      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38434      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38436      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 556.7ns 
38438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38438      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111ns 
38439      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40800      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
40800      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41596      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 582.31ns 
41599      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41599      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.7ns 
41600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43945      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
43946      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44712      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44714      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 536.71ns 
44717      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44717      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.2ns 
44719      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47091      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
47091      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47873      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.26ms 
47877      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47879      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.82ms 
47880      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
50240      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
51019      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
51086      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.58ms 
51092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
51093      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.6ns 
51096      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53448      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
53449      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
54229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54460      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 222.1ms 
54464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54464      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375ns 
54465      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56810      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
56811      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57598      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57603      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
57605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57605      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93ns 
57607      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59972      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
59973      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60715      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60718      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
60720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60720      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.9ns 
60721      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63073      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
63075      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63879      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.24ms 
63882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63882      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325ns 
63883      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66255      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
66255      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
67022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
67036      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.44ms 
67039      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
67040      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.5ns 
67041      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69367      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
69368      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
70139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
70154      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.36ms 
70157      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
70158      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.35ms 
70163      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72522      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
72523      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
73264      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
73279      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.08ms 
73282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
73282      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.6ns 
73283      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75668      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
75668      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
76430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
76444      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.13ms 
76447      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
76447      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337.7ns 
76448      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78772      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
78772      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
79552      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
79574      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.96ms 
79576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
79576      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.3ns 
79577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81930      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
81931      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
82671      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
82679      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.88ms 
82680      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
82681      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.9ns 
82683      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85039      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
85040      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
85808      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
85856      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.85ms 
85858      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
85859      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256.8ns 
85860      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88193      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
88193      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
88954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
89005      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.99ms 
89008      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
89009      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 639.4ns 
89010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91331      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
91331      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
92093      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
92134      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.94ms 
92136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
92136      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.2ns 
92137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94485      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
94486      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
95227      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
95234      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
95237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
95237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.2ns 
95238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97571      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
97571      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
98330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
98343      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.08ms 
98344      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
98344      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.6ns 
98345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
100658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
101414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
101425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.36ms 
101426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
101426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.3ns 
101427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
103738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
104497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
104504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.31ms 
104512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
104512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 235.3ns 
104513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
106877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
107618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
107626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.57ms 
107627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
107627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns 
107628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
110006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
110766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
110773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.11ms 
110775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
110775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.9ns 
110776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
113110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
113867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
113871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
113872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
113872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
113873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
116211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
116946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
116956     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.92ms 
116958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
116958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.1ns 
116959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
119302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
120060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
120112     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.48ms 
120114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
120114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.9ns 
120115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
122445     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
123206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
123224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.57ms 
123226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
123227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.5ns 
123227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
125581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
126339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
126357     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.14ms 
126359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
126359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.5ns 
126360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
128701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
129437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
129456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.22ms 
129457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
129457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.2ns 
129458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
131811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
132576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
132593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14ms 
132595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
132596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321.8ns 
132597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
134920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
135678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
135718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.99ms 
135720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
135721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.9ns 
135722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
138041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
138798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
138801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
138803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
138803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.6ns 
138804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
141143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
141890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
141894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
141896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
141896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
141897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
144243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
145000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
145008     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.35ms 
145011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
145011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.5ns 
145012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
147341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
148099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
148107     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.86ms 
148109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
148109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.1ns 
148110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
150425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
151187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
151207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.35ms 
151208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
151208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
151209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
153562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
154295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
154302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.51ms 
154304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
154304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.6ns 
154305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
156633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
157403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
157406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
157408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
157408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.5ns 
157409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
159743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
160504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
160508     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
160510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
160510     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
160510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
162848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
163581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
163585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
163587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
163587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
163588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
165919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
166675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
166746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.49ms 
166750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
166750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 310.3ns 
166751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
169079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
169838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
169918     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.79ms 
169920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
169920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.9ns 
169921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
172258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
173016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
173020     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
173021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
173021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
173022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
175365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
176098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
176136     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.19ms 
176139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
176139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 554.3ns 
176140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
178487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
179247     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
179277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.04ms 
179278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
179278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
179279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
181609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
182363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
182366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
182376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
182376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.9ns 
182381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
184714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
185468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
185607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 127.91ms 
185609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
185610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 285.9ns 
185610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
187945     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
188699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
188710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.95ms 
188712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
188712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
188713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
191020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
191776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
191788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
191790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
191790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
191791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
194089     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
194845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
194861     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
194863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
194863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
194864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
197184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
197914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
197930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.97ms 
197933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
197933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.3ns 
197934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
200276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
201031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
201035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
201037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
201037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.3ns 
201037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
203342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
204097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
204102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
204103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
204103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
204104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
206414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
207174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
207196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.16ms 
207197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
207198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 915.81ns 
207199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
209537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
210270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
210287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.81ms 
210288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
210288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
210289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
212619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
213374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
213390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.2ms 
213391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
213391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
213392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
215712     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
216465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
216469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.66ms 
216470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
216470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
216471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
218774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
219530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
219534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
219536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
219536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
219537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
221868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
222599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
222605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
222606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
222606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
222607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
224928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
225687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
225690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
225692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
225692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
225692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
228004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
228760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
228762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 719.61ns 
228763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
228763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
228764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
231074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
231826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
231830     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.26ms 
231831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
231831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
231832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
234161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
234920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
234922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 995.31ns 
234923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
234923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
234924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
237229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
237982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
238030     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.17ms 
238032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
238032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.5ns 
238033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
240345     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
241098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
241141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.26ms 
241143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
241143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
241143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
243462     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
244191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
244223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.62ms 
244225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
244225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
244226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
246546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
247298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
247344     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.28ms 
247346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
247346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240ns 
247347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
249668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
250421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
250453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.93ms 
250454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
250455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.5ns 
250455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
252750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
253505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
253559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.6ms 
253560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
253560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
253561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
255890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
256623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
256652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.65ms 
256655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
256655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.2ns 
256656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
258994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
259748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
259768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.68ms 
259770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
259770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
259771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
262068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
262820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
262844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.34ms 
262846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
262846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.7ns 
262847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
265174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
265905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
265925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.06ms 
265926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
265926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
265927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
268244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
268996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
269024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.13ms 
269026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
269026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
269026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
271332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
272085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
272110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.92ms 
272111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
272111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.1ns 
272112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
274420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
275175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
275201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.59ms 
275203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
275203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
275204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
277520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
278249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
278272     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.2ms 
278274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
278274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
278275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
280590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
281341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
281362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.2ms 
281363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
281364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
281364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
283687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
284438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
284464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.71ms 
284465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
284465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
284466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
286758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
287507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
287531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.33ms 
287533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
287533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
287533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
289849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
290607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
290615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.65ms 
290616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
290616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
290617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
292919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
293672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
293689     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.29ms 
293690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
293690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
293691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
295992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
296747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
296751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
296752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
296752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
296753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
299075     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
299804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
299807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 611.21ns 
299808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
299808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.9ns 
299809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
302123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
302882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
302885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 804.61ns 
302887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
302887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
302888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
305187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
305940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
305947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ms 
305948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
305948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
305949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
308241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
308994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
309000     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.03ms 
309001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
309001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
309002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
311322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
312051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
312063     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.9ms 
312065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
312065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
312065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
314381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
315136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
315139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
315140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
315140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
315141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
317438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
318192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
318194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 622.9ns 
318196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
318196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
318196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
320491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
321243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
321249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.69ms 
321250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
321250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
321251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
323566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
324295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
324297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.5ns 
324299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
324299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
324299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
326614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
327375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
327377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 571.9ns 
327378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
327378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
327379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
329678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
330430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
330432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 591.4ns 
330433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
330433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
330434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
332727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
333482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
333486     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.91ms 
333487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
333488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.7ns 
333488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
335810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
336540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
336579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.59ms 
336580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
336580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
336581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
338872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
339626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
339630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
339631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
339631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
339632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
341930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
342683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
342690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
342691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
342691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
342692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
345008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
345739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
345744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
345745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
345745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
345745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
348068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
348821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
348836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
348838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
348838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
348838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
351148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
351903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
351907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
351908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
351908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
351909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
354215     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
354972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
354975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
354976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
354976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
354977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
357290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
358019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
358023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
358024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
358024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.2ns 
358025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
360339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
361093     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
361110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.72ms 
361112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
361112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
361112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363418     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
363419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
364172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
364176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 594.8ns 
364178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
364178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
364179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
366487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
367217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
367256     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.42ms 
367257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
367257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
367258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
369574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
370329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
370336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
370337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
370338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.1ns 
370338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
372639     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
373392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
373414     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.54ms 
373415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
373415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
373416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
375740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
376470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
376491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.78ms 
376492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
376492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
376493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
378821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
379576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
379601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.1ms 
379602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
379602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
379603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
381904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
382660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
382662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 630.4ns 
382663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
382663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
382664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
384982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
385714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
385747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.22ms 
385749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
385749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
385749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
388059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
388814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
388817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
388819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
388819     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
388819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
391138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
391871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
391874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 806.71ns 
391875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
391875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
391876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
394190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
394944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
394947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 893.81ns 
394948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
394948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
394949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
397250     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
398009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
398012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
398013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
398013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
398014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
400330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
401084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
401087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
401088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
401088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
401089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
403380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
404137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
404147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ms 
404148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
404148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
404149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
406463     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
407197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
407211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.28ms 
407213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
407213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
407214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
409531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
410291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
410303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.18ms 
410304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
410304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
410305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
412631     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
413372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
413385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.73ms 
413386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
413386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
413387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
415722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
416485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
416489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.57ms 
416490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
416490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
416491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
418829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
419573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
419580     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.62ms 
419581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
419581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
419582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
421915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
421915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
422679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
422681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 706.5ns 
422682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
422682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
422683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
425016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
425760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
425763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
425765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
425765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
425765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
428100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
428860     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
428862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 940.01ns 
428863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
428863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
428864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
431190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
431931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
431942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.91ms 
431943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
431943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
431944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
434280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
435041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
435045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
435046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
435046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
435047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
437379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
438140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
438147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.79ms 
438149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
438149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.4ns 
438150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
440452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
441212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
441214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 702.5ns 
441215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
441215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
441216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
443537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
444296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
444298     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 612.8ns 
444300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
444300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
444300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
446595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
447356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
447360     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
447362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
447363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.6ns 
447363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
449688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
450452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
450455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
450456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
450456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
450456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
452783     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
453545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
453548     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
453549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
453549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.7ns 
453550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
455859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
456620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
456623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
456624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
456624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
456625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
458960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
459722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
459728     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.77ms 
459729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
459729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
459730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
462046     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
462785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
462789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
462790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
462790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
462791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
465107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
465868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
465879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ms 
465880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
465880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
465881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
468197     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
468955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
468957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 677.71ns 
468959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
468959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
468959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
471276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
472016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
472023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ms 
472024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
472024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
472025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
474335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
475096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
475100     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
475103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
475103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.5ns 
475104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
477420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
478179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
478181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 846.8ns 
478183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
478183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
478183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
480502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
481261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
481266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.21ms 
481268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
481268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
481268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
483578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
484338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
484341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
484342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
484342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
484343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
486662     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
487423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
487427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.98ms 
487428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
487428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
487429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
489750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
490511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
490515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.15ms 
490519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
490519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
490520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
492849     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
493609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
493614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.24ms 
493615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
493615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
493616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
495940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
496682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
496696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.11ms 
496697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
496697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
496698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
499030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
499792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
499807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
499808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
499809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
499809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
502133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
502895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
502905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.23ms 
502906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
502906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
502907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
505232     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
505994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
506004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ms 
506005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
506006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
506006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
508324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
509086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
509111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.38ms 
509112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
509112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
509113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
511433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
512193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
512218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.42ms 
512219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
512219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
512220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
514548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
515316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
515339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.82ms 
515340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
515340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
515341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
517673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
518414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
518428     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.92ms 
518429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
518429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
518430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520755     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
520755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
521521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
521560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.86ms 
521564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
521564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 239.6ns 
521565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
523916     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
524680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
524726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.58ms 
524728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
524728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.1ns 
524729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
527066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
527830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
527868     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.64ms 
527869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
527869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
527870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530203     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
530203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
530968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
531015     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.67ms 
531017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
531017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226ns 
531018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
533341     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
534106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
534148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.9ms 
534150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
534150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
534151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
536476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
537244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
537358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 107.4ms 
537360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
537360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
537360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539688     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
539688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
540450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
540458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
540459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
540459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
540460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
542773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
543534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
543541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.68ms 
543542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
543543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
543543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
545871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
546635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
546640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
546641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
546641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
546642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
548964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
549727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
549745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.19ms 
549746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
549746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
549747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
552066     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
552830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
552840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.63ms 
552842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
552842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
552842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
555166     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
555932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
555935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
555936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
555936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
555937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558257     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
558257     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
559021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
559037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
559039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
559039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
559039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
561379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
562121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
562137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.83ms 
562139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
562139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
562140     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
564489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
565250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
565269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.38ms 
565270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
565270     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
565271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
567591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
568355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
568358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
568359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
568359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
568360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
570680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
571440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
571446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
571447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
571447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
571448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
573764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
574524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
574530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.55ms 
574531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
574531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
574532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576839     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
576839     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
577599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
577606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.21ms 
577607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
577607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
577608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
579912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
580673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
580742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.28ms 
580743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
580744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
580744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
583092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
583859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
583885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.1ms 
583887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
583887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
583887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
586211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
586971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
586992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.98ms 
586994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
586994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
586995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
589323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
590087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
590089     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 296.7ns 
590090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
590090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
590091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
592406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
593166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
593358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 181.4ms 
593360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
593360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.4ns 
593361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
595710     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
596478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
596536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.93ms 
596541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
596541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89ns 
596541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
598900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
599663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
599665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 323.4ns 
599667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
599667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 232.7ns 
599668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
601998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
602760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
602762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 382.3ns 
602763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
602763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
602764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
605074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
605840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
605842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 407.7ns 
605843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
605843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
605844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
608171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
608933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
608935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 544.3ns 
608936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
608937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
608937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
611247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
612006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
612109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 100.63ms 
612110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
612111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.8ns 
612111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
614436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
615197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
615245     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.26ms 
615246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
615246     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
615248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
617621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
618385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
618387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ns 
618414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
618453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
618470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
618475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
618480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
618483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
618484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
618486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
618489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
618491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
618493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
618494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
618652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
618654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
618655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
618656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
618657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
618769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
618770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
618771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
618773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
618774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
618775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
618930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
618932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
618933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
618934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
618935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
618936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
619086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
619088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
619089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
619089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
619090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
619092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
619099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
619099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
619100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
619102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
619103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
619104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
619110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
619111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
619112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
619113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
619114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
619115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
619253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
619254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
619256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
619380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
619382     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)'' 
619384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
619386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
619387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
619388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
619388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
619389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
619393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
619394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
619396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
619396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
619397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
619509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
619513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
619515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
619516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
619516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
619517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
619518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
619646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
619648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
619649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
619650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
619651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
619652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
619652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
619654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
619756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
619758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
619900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
619905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
619910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
619911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
619912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
619913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
619914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
619914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
619915     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
619916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
619926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
619931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
620064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
620066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
620067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
620068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
620069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
620069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
620070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
620071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
620131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
620137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
620246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
620247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
620250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
620251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
620252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
620253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
620395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
620400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
620401     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)'' 
620403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
620404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
620405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
620406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
620406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
620416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
620418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
620419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
620420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
620563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
620565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
620566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
620566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
620567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
620568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
620704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
620706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
620707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
620708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
620709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
620710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
620710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
620711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
620813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
620814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
620897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
620898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
620899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
620903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
620908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
620912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
621055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
621056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
621057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
621058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
621070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
621159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
624795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
624797     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)'' 
624803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
624804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
624805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
624805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
624807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
624815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
624817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
624818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
624819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
624820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
624913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
624917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
624918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
624919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
624920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
624921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
624922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
625017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
625019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
625020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
625021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
625022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
625023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
625023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
625024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
625104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
625106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
625188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
625193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
625197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
625198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
625199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
625200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
625211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
625302     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
625304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
625304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
625306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
625386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
625396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
625397     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)'' 
625399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
625400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
625401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
625401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
625402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
625413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
625415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
625416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
625417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
625417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
625508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
625510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
625512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
625512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
625513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
625609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
625614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
625615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
625616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
625616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
625617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
625618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
625720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
625721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
625722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
625724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
625724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
625725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
625725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
625727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
625728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
625728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
625730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
625730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
625731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
625731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
625732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
625823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
625824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
625831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
625912     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
625996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
625997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
625999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
625999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
626000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
626001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
626001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
626002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
626003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
626092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
626099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
626192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
626193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
626194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
626196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
626196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
626197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
626197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
626198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
626203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
626204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
626287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
626293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
626299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
626457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
626458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
626459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
626460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
626461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
626461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
626462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
626463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
626520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
626521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
626522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
626523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
626524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
626529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
626535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
626656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
626747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
626748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
626749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
626750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
626922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
627012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
627013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
630203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
630208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
630209     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
630210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
630210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
630328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
630329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
630330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
630331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
630331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
630440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
633600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
637004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
637008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
637009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
637010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
637011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
637127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
637128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
637129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
637130     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)' ...' 
637131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
638281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
638281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
638282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
640683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
640683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
641461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
641462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
641462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
641468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
641479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
641482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
641484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
641484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
641488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
641489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
641492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
641494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
641495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
641503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
641505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
641505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
641550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
641551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
641551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
641552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
641552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
641613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
641614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
641615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
641616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
641616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
641619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
641620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
641620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
641621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
641622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
641623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
641702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
641703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
641703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
641704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
641705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
641706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
641790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
641791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
641791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
641792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
641793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
641794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
641794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
641795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
641796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
641796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
641796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
641797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
641797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
641798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
641799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
641799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
641800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
641800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
641801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
641804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
641840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
641841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
641898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
641899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
641901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
641902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
641903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
641904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
641955     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
641958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
641959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
641960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
641962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
641962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
641963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
642014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
642017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
642020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
642082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
642146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
642146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 220.7ns 
642147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
644614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
645473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
645527     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.95ms