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

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

tests
0

failures
0

ignored
10m44.36s

duration
100%

successful

Tests

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

Standard output

684        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
714        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 12.61ms 
932        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
947        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)

1814       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1816       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1817       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1817       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3458       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8923       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.99s 
8983       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9018       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.8ns 
9029       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9030       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.4ns 
9033       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11815      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
11817      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12795      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.78ms 
12804      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12804      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.2ns 
12806      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15462      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.66s 
15462      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16325      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16338      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.43ms 
16342      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16343      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.9ns 
16345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18939      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
18940      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19830      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19842      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.21ms 
19848      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19849      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 498.7ns 
19851      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22375      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
22375      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23191      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23196      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
23200      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23201      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 831.9ns 
23203      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25646      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
25647      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26450      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26488      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.44ms 
26492      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26492      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 645.7ns 
26494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28938      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
28939      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29714      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29732      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.99ms 
29736      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29737      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 495.3ns 
29738      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32190      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
32191      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32971      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 856.9ns 
32977      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32978      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.1ns 
32979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35437      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
35438      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36204      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36207      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 662.3ns 
36210      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36210      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.6ns 
36212      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
38667      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
38668      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39449      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39454      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.45ms 
39461      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39461      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 370.2ns 
39463      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41889      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
41889      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
42691      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
42698      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
42702      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
42703      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 436.7ns 
42705      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45104      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
45105      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
45887      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
45890      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 669.1ns 
45892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
45893      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 465.1ns 
45894      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48324      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
48324      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49106      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
49143      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.63ms 
49149      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
49150      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 598.4ns 
49152      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51544      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
51545      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
52326      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
52379      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.07ms 
52381      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
52381      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 152.8ns 
52384      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
54758      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
54758      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
55532      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
55681      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 140.42ms 
55684      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
55685      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 404.1ns 
55686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58052      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
58052      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
58829      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
58834      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.36ms 
58836      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
58836      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.6ns 
58837      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61203      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
61203      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
61980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
61983      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
61986      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
61986      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.9ns 
61987      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64342      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
64343      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
65118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
65153      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.42ms 
65156      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
65156      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.8ns 
65157      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67528      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
67529      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
68306      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
68318      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.65ms 
68320      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
68320      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.6ns 
68321      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70725      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
70725      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
71504      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
71515      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.08ms 
71518      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
71518      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 374.8ns 
71520      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73892      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
73893      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
74676      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
74693      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.54ms 
74695      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
74696      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.3ns 
74697      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77078      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
77079      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
77856      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
77867      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.32ms 
77870      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
77871      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.9ns 
77872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80245      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
80245      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
81024      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
81042      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.46ms 
81044      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
81045      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 391.3ns 
81046      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83429      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
83429      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
84178      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
84184      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.7ms 
84189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
84189      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.4ns 
84191      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86577      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
86577      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
87333      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
87379      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.52ms 
87382      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
87382      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.5ns 
87383      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89770      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
89770      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
90519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
90563      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.48ms 
90566      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
90566      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.5ns 
90568      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92959      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
92960      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
93709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
93740      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.19ms 
93744      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
93746      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.65ms 
93747      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96157      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
96161      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
96915      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
96923      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
96925      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
96926      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.8ns 
96927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99317      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
99318      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
100064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
100075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.7ms 
100077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
100077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.2ns 
100078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
102447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
103215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
103225     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.21ms 
103228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
103229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.7ns 
103230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
105610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
106376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
106383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.46ms 
106384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
106385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.4ns 
106385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
108741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
109511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
109518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.24ms 
109519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
109519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.1ns 
109520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
111867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
112639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
112645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.22ms 
112647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
112647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.9ns 
112647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
115000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
115768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
115772     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
115773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
115773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
115774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
118122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
118897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
118921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.74ms 
118924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
118924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 363.6ns 
118928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
121305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
122087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
122177     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.68ms 
122178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
122179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns 
122179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
124557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
125331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
125368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.86ms 
125371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
125371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.6ns 
125372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
127756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
128550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
128568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.33ms 
128570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
128570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 160.2ns 
128571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
130957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
131727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
131747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.07ms 
131748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
131748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.9ns 
131749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
134108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
134879     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
134895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.74ms 
134897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
134897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.1ns 
134898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
137247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
138021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
138057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.57ms 
138059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
138060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 321ns 
138061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
140423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
141170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
141173     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
141175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
141175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99ns 
141176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
143551     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
144299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
144303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.46ms 
144305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
144305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.2ns 
144306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
146692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
147441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
147448     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
147450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
147450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.2ns 
147451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
149845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
150590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
150598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.52ms 
150599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
150599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
150600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
152972     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
153749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
153766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.75ms 
153768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
153768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.6ns 
153769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
156129     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
156904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
156912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ms 
156914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
156914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.1ns 
156914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
159256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
160028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
160031     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
160038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
160038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.7ns 
160040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
162400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
163177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
163181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
163182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
163182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.6ns 
163183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
165538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
166309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
166312     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
166314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
166314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.9ns 
166315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
168676     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
169442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
169501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.27ms 
169503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
169503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.7ns 
169504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
171862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
172639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
172714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.37ms 
172718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
172718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 332.8ns 
172720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
175092     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
175864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
175867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
175870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
175870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 286.4ns 
175871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
178246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
179021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
179055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.4ms 
179057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
179057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
179058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
181433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
182196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
182218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.63ms 
182220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
182220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.3ns 
182221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
184562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
185326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
185329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
185330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
185330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
185331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
187678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
188449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
188560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 101.24ms 
188562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
188562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 
188563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
190930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
191695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
191705     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.38ms 
191708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
191708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.5ns 
191711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
194057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
194822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
194829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.47ms 
194832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
194832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.3ns 
194833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
197171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
197938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
197953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.91ms 
197954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
197955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85ns 
197955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
200351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
201096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
201108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.93ms 
201111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
201111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.4ns 
201112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
203473     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
204215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
204219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
204220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
204220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
204221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
206585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
207327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
207331     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
207332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
207332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
207333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
209724     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
210465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
210480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.01ms 
210485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
210485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.6ns 
210486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
212854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
213598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
213611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.91ms 
213613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
213613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
213614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
215957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
216724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
216736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.06ms 
216737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
216737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
216738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
219100     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
219868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
219872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
219873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
219873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
219874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
222216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
222988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
222991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
222992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
222992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
222993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
225342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
226108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
226113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.25ms 
226114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
226114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
226115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
228476     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
229243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
229246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 940.61ns 
229249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
229249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.7ns 
229250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
231601     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
232370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
232372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 533.5ns 
232373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
232373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
232374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
234709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
235473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
235476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
235477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
235478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.2ns 
235478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
237848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
238620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
238622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 736.71ns 
238624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
238624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
238624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
240970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
241733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
241765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.5ms 
241767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
241768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.6ns 
241769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
244140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
244906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
244939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.24ms 
244941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
244941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
244942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
247282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
248045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
248068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.66ms 
248069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
248070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
248070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
250413     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
251183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
251216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.56ms 
251218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
251218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
251218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
253557     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
254294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
254313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.84ms 
254315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
254315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
254315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
256651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
257391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
257430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.21ms 
257432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
257432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
257433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
259797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
260537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
260556     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.35ms 
260558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
260558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
260558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
262961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
263729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
263744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.21ms 
263746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
263747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.5ns 
263748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
266149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
266922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
266937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.01ms 
266938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
266938     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
266939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
269277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
270043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
270055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.12ms 
270057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
270057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
270058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
272385     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
273151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
273167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.85ms 
273169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
273169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
273170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
275501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
276267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
276283     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.62ms 
276284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
276284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.9ns 
276285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
278630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
279432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
279451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.62ms 
279454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
279454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.2ns 
279455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
281805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
282569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
282584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms 
282586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
282586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
282586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
284927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
285693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
285707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.79ms 
285710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
285710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.2ns 
285711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
288043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
288044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
288808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
288823     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.05ms 
288825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
288825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
288826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
291171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
291952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
291968     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.27ms 
291969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
291969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
291970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
294328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
295100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
295106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
295107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
295107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
295108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
297452     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
298229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
298241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.13ms 
298242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
298242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
298243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
300616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
301381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
301385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
301386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
301387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
301387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
303721     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
304490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
304492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 581.7ns 
304494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
304494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
304494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
306835     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
307604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
307608     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 667.3ns 
307609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
307609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
307610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
309941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
310681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
310688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
310689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
310689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
310690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
313041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
313783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
313789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.3ms 
313791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
313791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207ns 
313792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
316157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
316897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
316907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.47ms 
316908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
316908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
316909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
319275     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
320022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
320026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
320027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
320027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
320028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
322397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
323139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
323141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 487.6ns 
323143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
323143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.7ns 
323144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
325484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
326252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
326262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
326264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
326265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.9ns 
326266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
328615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
329383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
329385     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 647.6ns 
329387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
329387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
329388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
331734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
332508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
332510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 526.4ns 
332512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
332512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
332513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
334864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
335630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
335632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 546.3ns 
335633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
335633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
335634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
338002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
338769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
338773     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
338774     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
338775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
338775     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
341115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
341880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
341887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
341889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
341889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
341889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
344224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
344990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
344993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.64ms 
344995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
344995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.4ns 
344996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
347332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
347332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
348116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
348122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.56ms 
348125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
348125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.5ns 
348126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
350469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
351234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
351238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
351240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
351240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
351240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
353595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
354361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
354373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.37ms 
354374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
354374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
354375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
356719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
357486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
357490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
357491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
357491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
357492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
359831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
360598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
360601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
360602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
360602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
360603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
362934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
363675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
363679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
363680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
363680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
363681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
366026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
366766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
366778     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.37ms 
366780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
366780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.7ns 
366781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
369131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
369873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
369878     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 339.6ns 
369880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
369880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
369881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
372229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
372973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
372999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.61ms 
373000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
373001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.4ns 
373001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
375351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
376095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
376098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
376100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
376100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
376101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
378425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
379188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
379203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.22ms 
379205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
379205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
379206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
381550     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
382322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
382337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.92ms 
382338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
382338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.4ns 
382339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
384683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
384683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
385449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
385467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.44ms 
385469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
385469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
385470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
387800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
388574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
388577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 611.2ns 
388582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
388582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105ns 
388583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
390918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
391680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
391685     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
391687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
391687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
391688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
394002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
394765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
394769     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
394770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
394770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
394771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
397085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
397848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
397851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 743.9ns 
397852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
397852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
397853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
400174     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
400940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
400943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 785.6ns 
400945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
400945     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.5ns 
400946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
403274     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
404041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
404045     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
404046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
404046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
404047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
406427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
407196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
407200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
407202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
407202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
407204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
409553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
410330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
410340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.58ms 
410342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
410342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
410342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
412690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
413460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
413467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.73ms 
413468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
413468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.7ns 
413469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
415799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
416546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
416552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 
416554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
416554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
416554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
418969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
419779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
419788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.82ms 
419789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
419789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.7ns 
419790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
422176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
422933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
422937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
422939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
422939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
422940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
425324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
426077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
426081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.47ms 
426083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
426083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
426083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
428451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
429209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
429213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
429215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
429215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
429216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
431592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
432347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
432349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.1ms 
432351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
432351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
432352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
434740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
435518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
435520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 953.5ns 
435522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
435522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
435522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
437892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
438647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
438656     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.81ms 
438658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
438658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
438658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
441038     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
441793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
441796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
441798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
441798     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
441799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
444171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
444925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
444931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.64ms 
444932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
444932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
444933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
447324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
448081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
448083     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 846.1ns 
448085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
448085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
448085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
450479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
451234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
451236     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 743.9ns 
451237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
451237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
451238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
453611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
454370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
454373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
454375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
454375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.5ns 
454375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
456752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
457508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
457510     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 796.1ns 
457512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
457512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
457512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
459876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
460634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
460637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
460638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
460638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
460639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
463026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
463802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
463805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
463806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
463806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
463807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
466149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
466922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
466926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
466928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
466928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
466928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
469265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
470042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
470044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 871.3ns 
470046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
470046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
470047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
472390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
473167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
473187     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.97ms 
473188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
473188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.6ns 
473189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
475548     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
476325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
476327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 702ns 
476328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
476328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.3ns 
476329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
478701     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
479483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
479489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
479490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
479490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.9ns 
479491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
481868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
482643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
482646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 887.1ns 
482647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
482647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
482648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
485019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
485019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
485796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
485798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 753.1ns 
485800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
485800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
485800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
488224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
488224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
488986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
488989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
488991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
488991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
488992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
491365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
492121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
492124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 911.9ns 
492125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
492125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.4ns 
492126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494551     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
494552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
495333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
495339     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
495341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
495341     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.7ns 
495342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
497688     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
498466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
498469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
498471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
498471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
498471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
500827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
501607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
501611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
501613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
501613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
501615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
503969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
504743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
504750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
504751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
504752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
504752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
507109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
507859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
507867     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
507868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
507868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.6ns 
507869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
510234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
511011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
511017     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.12ms 
511018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
511019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
511019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
513378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
514157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
514163     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.31ms 
514165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
514165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
514166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
516499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
517272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
517282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.77ms 
517284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
517284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.61ns 
517285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
519611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
520385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
520395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.58ms 
520397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
520397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
520398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
522812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
522815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
523565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
523574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.98ms 
523576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
523576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
523576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
525928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
525928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
526707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
526714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
526715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
526715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
526716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
529071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
529071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
529849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
529869     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.51ms 
529870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
529870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
529871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
532195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
532195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
532973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
532995     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.52ms 
532996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
532996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.6ns 
532997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
535351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
536103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
536122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.78ms 
536123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
536123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90ns 
536124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
538495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
539281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
539299     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.16ms 
539301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
539301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
539301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
541645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
541645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
542422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
542440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.28ms 
542442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
542442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
542443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
544793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
544794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
545546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
545599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.68ms 
545602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
545602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.31ns 
545603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
547966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
548744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
548753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
548756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
548757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
548757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
551090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
551861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
551866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.98ms 
551867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
551867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
551868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
554217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
554968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
554972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.94ms 
554973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
554973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
554974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
557325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
558101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
558114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.96ms 
558115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
558115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
558116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
560486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
561270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
561277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
561279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
561279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
561279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
563638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
564392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
564395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
564396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
564396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
564397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
566772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
567548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
567558     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.33ms 
567560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
567560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.3ns 
567560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
569915     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
570695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
570706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ms 
570708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
570708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
570708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
573070     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
573852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
573866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.49ms 
573868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
573868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.41ns 
573869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
576208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
576980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
576983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 976.92ns 
576984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
576984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
576985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
579323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
580078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
580081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
580083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
580083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.3ns 
580084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
582435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
583209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
583215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms 
583216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
583216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.8ns 
583217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
585537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
586310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
586314     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.69ms 
586316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
586316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
586317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
588647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
589418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
589458     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.9ms 
589460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
589460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
589461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
591815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
591815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
592599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
592618     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.16ms 
592620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
592620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.7ns 
592621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
594994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
595766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
595777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.59ms 
595779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
595779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
595779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
598112     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
598891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
598894     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 187.3ns 
598895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
598895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
598896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
601252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
602027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
602105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 68.26ms 
602106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
602107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
602107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
604446     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
605221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
605253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.62ms 
605254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
605254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
605255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
607621     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
608398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
608400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 203.5ns 
608405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
608405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.6ns 
608405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
610747     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
611527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
611529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 232.21ns 
611530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
611530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
611531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
613885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
614661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
614663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 223.8ns 
614664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
614664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
614665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
617001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
617777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
617779     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 358.61ns 
617780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
617780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
617781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
620145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
620920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
621029     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
621036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.92ms 
621038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
621038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
621039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
623388     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
624163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
624211     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
624212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.36ms 
624218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
624218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.3ns 
624220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
626593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
626593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
627370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
627372     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.4ns 
627400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
627455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
627475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
627483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
627503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
627504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
627507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
627508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
627515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
627516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
627521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
627523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
627758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
627759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
627760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
627761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
627762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
627909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
627910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
627913     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
627914     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
627916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
627917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
628080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
628082     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
628084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
628085     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
628086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
628091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
628242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
628243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
628245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
628245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
628246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
628247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
628255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
628256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
628257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
628261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
628263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
628264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
628274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
628275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
628276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
628277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
628277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
628278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
628422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
628422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
628425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
628566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
628567     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)'' 
628568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
628570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
628571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
628572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
628573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
628576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
628580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
628581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
628583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
628584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
628585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
628707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
628711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
628713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
628714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
628716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
628717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
628718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
628872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
628873     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
628875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
628878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
628879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
628879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
628881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
628882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
628986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
628988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
629077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
629081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
629087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
629088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
629091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
629093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
629093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
629094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
629095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
629095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
629104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
629109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
629220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
629223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
629230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
629232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
629233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
629234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
629234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
629235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
629298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
629304     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
629399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
629400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
629402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
629404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
629405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
629406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
629538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
629543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
629545     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)'' 
629549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
629550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
629551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
629552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
629552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
629562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
629567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
629568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
629569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
629657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
629659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
629660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
629661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
629662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
629664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
629761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
629763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
629765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
629766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
629767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
629768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
629769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
629770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
629885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
629886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
629957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
629958     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
629959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
629964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
629968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
629973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
630087     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
630088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
630089     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
630090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
630100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
630180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
633806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
633807     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)'' 
633811     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
633813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
633814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
633825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
633826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
633836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
633837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
633838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
633839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
633840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
633936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
633940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
633941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
633942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
633943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
633943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
633944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
634037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
634039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
634040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
634041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
634042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
634042     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
634043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
634044     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
634119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
634120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
634193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
634197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
634202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
634203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
634204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
634205     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
634215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
634293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
634294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
634295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
634296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
634366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
634376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
634377     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)'' 
634378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
634380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
634381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
634382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
634382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
634393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
634394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
634395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
634396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
634397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
634484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
634485     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
634486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
634487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
634488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
634625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
634630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
634631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
634632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
634633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
634633     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
634634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
634730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
634731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
634733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
634734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
634734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
634735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
634736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
634736     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
634737     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
634738     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
634739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
634740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
634740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
634741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
634742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
634827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
634829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
634835     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
634918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
634997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
634998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
634999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
635000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
635001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
635002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
635002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
635003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
635003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
635086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
635093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
635180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
635181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
635182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
635183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
635183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
635183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
635184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
635184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
635190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
635190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
635268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
635274     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
635279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
635377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
635377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
635378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
635379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
635380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
635380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
635380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
635381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
635434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
635435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
635436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
635436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
635437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
635443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
635448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
635561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
635649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
635650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
635650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
635651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
635815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
635903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
635903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
638855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
638859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
638860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
638861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
638862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
638974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
638975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
638976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
638977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
638977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
639081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
641897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
644973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
644977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
644978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
644979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
644979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
645091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
645091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
645092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
645093     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)' ...' 
645094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
646210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
646210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
646211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
648609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
649410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
649412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.8ns 
649412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
649422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
649432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
649434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
649436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
649437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
649443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
649443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
649448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
649449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
649451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
649462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
649463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
649464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
649527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
649528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
649529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
649529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
649530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
649610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
649611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
649611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
649612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
649613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
649617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
649618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
649618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
649619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
649620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
649621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
649720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
649721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
649722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
649722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
649723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
649724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
649877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
649878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
649879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
649879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
649880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
649881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
649881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
649882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
649882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
649883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
649883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
649884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
649884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
649885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
649885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
649886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
649886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
649887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
649888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
649891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
649932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
649933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
649999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
650000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
650001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
650002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
650003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
650004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
650064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
650066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
650067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
650068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
650069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
650070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
650071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
650130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
650133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
650136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
650211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
650274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
650274     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.4ns 
650275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
652614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
652614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
653392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
653408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.73ms