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

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

tests
0

failures
0

ignored
10m35.15s

duration
100%

successful

Tests

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

Standard output

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

1602       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1604       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1607       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1607       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2842       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7842       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.03s 
7900       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7931       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.6ns 
7944       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7945       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 931.31ns 
7949       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10764      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
10767      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11654      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11678      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.28ms 
11686      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
11687      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 151.1ns 
11688      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14224      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
14226      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15073      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15088      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.03ms 
15092      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15093      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.5ns 
15095      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17698      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.6s 
17700      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18534      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18540      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.13ms 
18542      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18542      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.1ns 
18543      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21033      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
21033      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
21827      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
21840      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.39ms 
21846      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
21847      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 887.18ns 
21849      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24271      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
24271      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25037      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25076      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.3ms 
25078      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25078      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.4ns 
25079      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27468      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
27468      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28229      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28247      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.84ms 
28249      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28249      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.4ns 
28250      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
30641      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
30641      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31399      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31402      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.4ns 
31403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31404      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.8ns 
31404      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33803      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
33803      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
34565      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
34570      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 671.71ns 
34572      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
34573      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 586.31ns 
34574      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36968      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
36968      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37731      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37734      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.11ns 
37735      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37736      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181.6ns 
37737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40129      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
40130      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
40886      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
40888      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 592.4ns 
40890      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
40890      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.3ns 
40891      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43274      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
43274      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44027      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44030      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 541.9ns 
44032      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44033      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.4ns 
44034      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46398      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
46399      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47160      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47250      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.19ms 
47251      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47252      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.7ns 
47252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49620      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
49620      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50367      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50399      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.35ms 
50402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50402      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.4ns 
50403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
52781      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53550      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
53766      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 207.05ms 
53770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
53770      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 401.81ns 
53772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56172      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
56172      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
56924      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
56929      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
56930      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
56930      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.3ns 
56931      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59291      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
59291      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60045      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60048      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
60051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60052      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.4ns 
60053      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62444      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
62444      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63190      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63228      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.12ms 
63230      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63230      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.4ns 
63231      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65577      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
65577      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66362      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.72ms 
66364      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66364      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.7ns 
66365      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68711      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
68712      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
69494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
69511      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.26ms 
69513      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
69515      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.55ms 
69519      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71857      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
71858      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
72630      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
72646      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.73ms 
72648      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
72648      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.4ns 
72650      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75007      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
75007      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
75780      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
75795      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.05ms 
75796      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
75796      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.4ns 
75797      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78129      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
78129      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
78892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
78916      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.56ms 
78918      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
78918      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.5ns 
78919      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81254      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
81254      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
82032      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
82035      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
82036      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
82037      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.6ns 
82038      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84366      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
84366      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
85141      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
85180      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.25ms 
85182      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
85182      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.2ns 
85183      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87516      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
87517      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
88281      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
88336      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.36ms 
88339      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
88340      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 337ns 
88341      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90692      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
90692      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
91462      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
91504      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.16ms 
91506      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
91506      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.9ns 
91507      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93844      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
93845      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
94614      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
94622      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
94623      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
94623      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 112.1ns 
94624      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97041      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
97042      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
97811      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
97823      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.09ms 
97825      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
97825      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
97826      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
100148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
100911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
100921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.28ms 
100923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
100923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.4ns 
100924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
103235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
103997     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
104004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.09ms 
104005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
104005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
104006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
106319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
107079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
107087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.15ms 
107088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
107088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.9ns 
107089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
109408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
110182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
110189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms 
110190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
110191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.3ns 
110191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
112521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
113284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
113287     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
113288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
113288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
113289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
115616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
116376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
116391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.61ms 
116392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
116392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns 
116393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
118722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
119486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
119535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.28ms 
119536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
119536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
119537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
121865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
122629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
122647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.98ms 
122649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
122649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.1ns 
122650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
124963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
125724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
125741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.43ms 
125744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
125744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 296ns 
125745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
128110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
128872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
128888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.86ms 
128890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
128890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.9ns 
128891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
131213     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
131977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
131994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.06ms 
131995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
131995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
131996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
134313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
134313     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
135077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
135119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.3ms 
135122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
135122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 308.2ns 
135123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
137443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
137443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
138206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
138211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
138212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
138213     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
138213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140530     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
140530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
141299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
141303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.41ms 
141304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
141305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.3ns 
141305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
143617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
144378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
144387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.04ms 
144389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
144389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.9ns 
144390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
146707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
147470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
147479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.38ms 
147480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
147480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
147481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
149807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
150565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
150583     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.91ms 
150584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
150584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.1ns 
150585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
152898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
153662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
153671     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.69ms 
153676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
153676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.8ns 
153676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
156006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
156006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
156784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
156788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
156791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
156791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 293.1ns 
156792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
159189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
159955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
159959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
159961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
159962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.7ns 
159963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
162282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
162282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
163045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
163050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
163052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
163052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.7ns 
163053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165375     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
165376     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
166134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
166213     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 70.57ms 
166214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
166214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.6ns 
166215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
168541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
169308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
169393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.99ms 
169394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
169394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103ns 
169395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
171719     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
172485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
172489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
172491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
172491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 250.8ns 
172492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
174819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
175584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
175641     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.9ms 
175644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
175649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 4.35ms 
175650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
177971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
177971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
178737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
178785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.23ms 
178787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
178787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
178788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
181107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
181869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
181871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
181873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
181873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
181874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
184280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
185046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
185186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 129.09ms 
185189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
185189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 264.6ns 
185190     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
187534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
188299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
188310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.38ms 
188311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
188311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
188312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
190632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
191395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
191404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.97ms 
191405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
191405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
191406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
193756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
193757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
194517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
194533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.22ms 
194534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
194534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
194535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
196853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
197610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
197622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.02ms 
197624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
197624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.8ns 
197625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
199940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
199940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
200693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
200697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
200698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
200698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
200699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
203013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
203772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
203776     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.59ms 
203777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
203777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
203778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
206115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
206875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
206897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.14ms 
206898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
206898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.4ns 
206899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
209221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
209985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
210005     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.68ms 
210009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
210009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.2ns 
210010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
212340     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
213100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
213115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.05ms 
213117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
213117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.6ns 
213118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
215437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
216198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
216201     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
216202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
216202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
216203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
218541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
219306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
219310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
219311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
219311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
219312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221619     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
221619     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
222391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
222397     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms 
222398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
222398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
222399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
224728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
225467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
225470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
225471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
225471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
225472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
227797     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
228532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
228534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.01ns 
228535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
228536     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
228536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
230870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
231606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
231610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
231611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
231611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
231612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
233941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
234678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
234681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 961.43ns 
234682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
234682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
234683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
237014     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
237751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
237796     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.52ms 
237797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
237797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
237798     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
240142     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
240878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
240912     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.48ms 
240914     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
240914     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
240915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
243249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
243984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
244013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.13ms 
244014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
244014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
244015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
246344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
247083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
247123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.39ms 
247124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
247124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
247125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
249459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
250195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
250224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.75ms 
250225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
250226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
250226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
252569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
253304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
253350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.82ms 
253351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
253351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
253352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
255699     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
256434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
256459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.31ms 
256460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
256460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
256461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
258794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
259528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
259546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.37ms 
259548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
259548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.9ns 
259548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
261887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
262622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
262644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.23ms 
262645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
262645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.8ns 
262646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
264997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
265732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
265750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.97ms 
265751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
265751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
265752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
268082     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
268817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
268843     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.63ms 
268844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
268844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
268845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
271185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
271922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
271945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.4ms 
271946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
271946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
271947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
274294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
275030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
275054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.54ms 
275055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
275055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
275056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
277401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
278144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
278168     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.89ms 
278171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
278171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 240.83ns 
278172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
280508     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
281242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
281262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.63ms 
281263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
281264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
281264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
283595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
284330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
284361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.55ms 
284363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
284363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.01ns 
284364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
286703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
287437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
287464     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.57ms 
287467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
287467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.81ns 
287468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
289804     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
290539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
290546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.4ms 
290548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
290548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.41ns 
290549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
292852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
293621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
293638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.99ms 
293639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
293639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53ns 
293640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
295944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
296703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
296706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
296708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
296708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.61ns 
296709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
299022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
299781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
299783     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 568.03ns 
299784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
299784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
299785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
302086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
302852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
302855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 715.2ns 
302857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
302857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
302858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
305161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
305923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
305930     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.48ms 
305931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
305931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
305932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
308243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
309006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
309012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.07ms 
309014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
309014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.31ns 
309015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
311330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
312091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
312103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.47ms 
312104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
312104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
312105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
314403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
315162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
315165     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
315167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
315167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
315167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317465     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
317465     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
318226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
318228     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 516.72ns 
318229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
318229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
318230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
320527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
321286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
321291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.49ms 
321293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
321293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
321293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
323590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
324356     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
324358     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 697.93ns 
324359     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
324359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
324360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
326664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
327425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
327427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 585.02ns 
327429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
327429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
327429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
329728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
329729     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
330488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
330490     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.52ns 
330491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
330491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
330491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
332791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
332791     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
333550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
333554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
333555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
333555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
333556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
335854     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
336611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
336627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.9ms 
336630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
336630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.51ns 
336631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
338936     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
339695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
339699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
339700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
339700     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
339701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
341999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
342760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
342767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ms 
342768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
342768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.6ns 
342769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
345064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
345825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
345829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.24ms 
345830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
345830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
345831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
348132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
348894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
348911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.4ms 
348912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
348912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
348913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
351220     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
351980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
351984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
351985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
351985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
351986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
354290     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
355047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
355051     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
355052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
355052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
355052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
357354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
358112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
358115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
358116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
358116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
358117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
360420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
361178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
361195     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.94ms 
361196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
361196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
361197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
363505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
364265     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
364269     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 548.22ns 
364271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
364271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
364272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
366579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
367341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
367379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.89ms 
367380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
367380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
367381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
369693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
369693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
370453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
370457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
370458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
370458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
370459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
372789     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
373547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
373567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.8ms 
373568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
373569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
373569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
375876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
375876     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
376637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
376657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.47ms 
376658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
376658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
376659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
378966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
379724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
379747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.21ms 
379749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
379749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
379750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
382064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
382823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
382825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 570.82ns 
382826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
382826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
382827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
385122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
385880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
385885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
385886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
385887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
385887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
388194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
388956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
388959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
388960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
388960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
388960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
391266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
392030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
392032     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 787.73ns 
392033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
392033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
392034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
394331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
395095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
395097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 872.83ns 
395098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
395098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.1ns 
395099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
397398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
397398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
398167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
398170     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
398171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
398171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
398172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
400478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
401241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
401244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
401245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
401245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
401246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
403540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
404303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
404313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.49ms 
404314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
404314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
404315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
406611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
407376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
407387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.51ms 
407388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
407388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
407389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
409689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
410454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
410465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.52ms 
410466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
410466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
410467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
412767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
413540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
413555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.28ms 
413557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
413557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.31ns 
413558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
415874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
415874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
416649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
416654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
416655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
416656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.21ns 
416657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
418961     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
419739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
419745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.44ms 
419747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
419747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
419747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
422054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
422827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
422829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707.5ns 
422830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
422830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
422831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
425131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
425903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
425906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
425907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
425907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
425907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
428210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
428983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
428985     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 955.53ns 
428987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
428987     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
428987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
431289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
432065     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
432075     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.66ms 
432077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
432077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
432077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
434382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
435157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
435162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.33ms 
435164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
435164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.91ns 
435165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
437471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
437471     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
438243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
438249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.65ms 
438251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
438251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
438251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
440552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
441327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
441329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 713.12ns 
441330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
441331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
441331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443622     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
443623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
444393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
444395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 633.72ns 
444396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
444396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
444397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446693     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
446693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
447467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
447471     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
447472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
447472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
447473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
449766     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
450538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
450540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
450542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
450542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
450542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
452853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
453602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
453605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
453606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
453606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
453607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
455927     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
456676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
456679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
456680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
456680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59ns 
456680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
459005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
459779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
459787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
459788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
459788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
459789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
462090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
462862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
462865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
462866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
462866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
462867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
465176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
465950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
465960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.53ms 
465962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
465962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
465962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
468259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
469030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
469033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 656.62ns 
469034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
469034     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
469034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
471327     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
472100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
472109     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.99ms 
472111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
472111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
472111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
474423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
475172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
475175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 843.63ns 
475176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
475176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
475176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
477493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
478242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
478244     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 748.92ns 
478245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
478245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
478246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
480560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
481332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
481336     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.03ms 
481337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
481338     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.7ns 
481338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
483635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
484407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
484410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
484411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
484412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
484412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
486705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
487476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
487480     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
487481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
487481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
487481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
489775     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
490550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
490553     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
490554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
490554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
490555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
492869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
492869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
493624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
493628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3ms 
493629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
493629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
493630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
495950     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
496723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
496736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.64ms 
496737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
496738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
496738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
499036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
499808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
499822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.53ms 
499823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
499823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
499824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
502127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
502899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
502911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.73ms 
502912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
502912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
502913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
505227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
505977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
505987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.44ms 
505988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
505988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
505989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
508325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
509097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
509124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.29ms 
509125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
509126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.1ns 
509126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
511432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
512206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
512230     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.57ms 
512231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
512231     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
512232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
514555     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
515305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
515327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.85ms 
515328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
515328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.2ns 
515329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
517651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
518423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
518436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.71ms 
518438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
518438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
518438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
520749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
521525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
521554     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.45ms 
521555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
521555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
521556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523855     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
523855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
524629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
524674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.2ms 
524675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
524675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
524676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526997     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
526997     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
527771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
527807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33ms 
527809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
527809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
527809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
530113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
530898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
530937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.13ms 
530939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
530939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
530939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
533258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
534006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
534047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.86ms 
534048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
534048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
534049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
536364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
537137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
537247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.88ms 
537248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
537248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
537249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
539554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
540326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
540333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
540335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
540335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
540335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
542647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
543420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
543427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.45ms 
543428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
543428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
543429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
545727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
546498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
546503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.46ms 
546504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
546504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
546505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
548822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
549571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
549588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
549589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
549589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
549590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
551907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
552678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
552688     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
552689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
552689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.8ns 
552690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
554983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
555756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
555760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
555761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
555761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
555762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
558083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
558858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
558874     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.18ms 
558875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
558875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
558876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
561176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
561949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
561967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.33ms 
561968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
561968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
561969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
564287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
565037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
565055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.09ms 
565057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
565057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
565057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
567378     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
568149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
568151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
568153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
568153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
568153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
570464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
571213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
571217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
571218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
571218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
571219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
573530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
574299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
574306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.72ms 
574307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
574307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
574307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
576625     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
577376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
577383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
577384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
577384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
577385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
579715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
580486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
580551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.37ms 
580552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
580552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
580553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582877     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
582878     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
583631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
583663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.87ms 
583665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
583665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.6ns 
583666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
585983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
586754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
586775     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.91ms 
586777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
586777     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
586777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
589091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
589844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
589846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 306.01ns 
589849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
589849     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177.8ns 
589850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
592186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
592957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
593140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 173.48ms 
593142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
593143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 198.9ns 
593143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
595468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
596244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
596292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.84ms 
596293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
596293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
596294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
598590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
599362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
599364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 348.71ns 
599365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
599366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.6ns 
599366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
601677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
602447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
602449     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 334.11ns 
602450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
602450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
602451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
604760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
605512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
605514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 352.91ns 
605515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
605516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.3ns 
605516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
607826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
608597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
608599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 458.31ns 
608600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
608600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
608600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
610907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
611676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
611751     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
611764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 85.6ms 
611766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
611766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.6ns 
611767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
614078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
614852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
614902     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
614903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.59ms 
614904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
614904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
614910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
617233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
618011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
618012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ns 
618037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
618081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
618102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
618109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
618116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
618119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
618120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
618124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
618130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
618132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
618136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
618137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
618359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
618361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
618362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
618363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
618364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
618502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
618504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
618507     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
618509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
618511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
618511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
618707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
618710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
618711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
618712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
618714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
618717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
618861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
618863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
618864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
618865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
618866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
618867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
618875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
618876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
618877     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
618880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
618881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
618882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
618891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
618892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
618894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
618895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
618896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
618897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
619030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
619032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
619033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
619153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
619154     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)'' 
619157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
619158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
619159     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
619161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
619162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
619164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
619168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
619170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
619171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
619172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
619172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
619278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
619282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
619283     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
619284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
619285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
619286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
619288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
619411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
619413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
619414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
619416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
619417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
619418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
619419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
619421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
619518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
619519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
619612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
619616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
619621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
619622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
619625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
619627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
619627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
619628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
619628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
619629     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
619639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
619643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
619746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
619747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
619749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
619751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
619751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
619752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
619752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
619754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
619810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
619816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
619938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
619940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
619942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
619943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
619944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
619945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
620094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
620099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
620100     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)'' 
620102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
620103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
620104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
620105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
620106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
620115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
620116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
620118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
620118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
620229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
620231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
620232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
620233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
620233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
620234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
620410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
620412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
620413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
620414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
620415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
620415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
620416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
620417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
620514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
620516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
620603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
620604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
620605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
620610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
620613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
620617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
620751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
620752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
620753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
620754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
620765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
620861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
624246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
624247     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)'' 
624252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
624253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
624254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
624254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
624256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
624263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
624264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
624265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
624266     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
624267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
624354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
624358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
624359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
624360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
624361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
624361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
624362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
624450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
624452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
624453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
624455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
624456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
624457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
624458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
624459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
624530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
624531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
624600     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
624604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
624608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
624610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
624610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
624611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
624623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
624699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
624700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
624701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
624702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
624772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
624782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
624783     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)'' 
624785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
624786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
624787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
624788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
624788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
624799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
624800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
624801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
624802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
624802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
624890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
624892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
624893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
624894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
624894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
625025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
625029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
625030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
625031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
625032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
625032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
625033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
625127     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
625129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
625130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
625131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
625132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
625132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
625133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
625134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
625135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
625136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
625137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
625138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
625138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
625139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
625140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
625222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
625223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
625229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
625303     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
625379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
625380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
625381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
625382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
625383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
625384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
625384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
625385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
625386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
625466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
625472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
625556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
625557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
625558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
625559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
625559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
625560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
625560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
625561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
625565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
625566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
625641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
625646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
625651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
625744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
625745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
625746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
625747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
625747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
625748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
625748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
625749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
625800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
625801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
625801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
625802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
625803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
625808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
625813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
625924     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
626008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
626009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
626009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
626010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
626168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
626251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
626252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
629096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
629101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
629102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
629102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
629103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
629211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
629212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
629213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
629214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
629214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
629314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
632034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
634976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
634980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
634981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
634982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
634983     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
635090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
635091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
635092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
635093     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)' ...' 
635095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
636167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
636167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.6ns 
636168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
638556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
639310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
639311     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 
639311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
639319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
639377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
639379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
639381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
639381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
639386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
639387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
639390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
639392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
639393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
639402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
639403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
639404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
639447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
639447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
639448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
639448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
639449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
639503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
639504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
639505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
639506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
639506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
639509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
639509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
639510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
639510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
639511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
639512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
639581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
639582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
639582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
639583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
639584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
639584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
639660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
639660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
639660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
639661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
639661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
639662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
639663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
639663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
639664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
639664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
639664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
639665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
639665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
639665     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
639666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
639666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
639666     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
639667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
639668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
639670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
639703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
639704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
639758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
639759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
639761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
639762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
639762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
639763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
639810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
639812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
639813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
639814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
639815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
639816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
639816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
639863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
639865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
639867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
639918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
639968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
639968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
639969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
642278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
643079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
643108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.32ms