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

198

tests

0

failures

0

ignored

10m31.66s

duration

100%

successful

Tests

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

Standard output

652        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
674        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 7.74ms 
902        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
914        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)

1796       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1798       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1801       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1801       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3167       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8193       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.29s 
8251       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8308       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35ns 
8320       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8320       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 499.8ns 
8324       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11055      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
11058      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
11976      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
11999      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.72ms 
12007      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12008      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132ns 
12009      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14630      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.62s 
14631      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15478      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.48ms 
15480      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15480      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.1ns 
15481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18039      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
18040      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
18897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
18913      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.04ms 
18914      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
18915      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.3ns 
18916      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21319      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
21319      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22119      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22124      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.77ms 
22126      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22126      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.8ns 
22127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24568      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
24568      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25403      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25471      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.66ms 
25474      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25474      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.4ns 
25475      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
27856      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
27857      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28636      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28670      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.6ms 
28674      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28674      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.3ns 
28675      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31062      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
31063      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
31890      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
31894      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 551.4ns 
31896      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
31896      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 326.6ns 
31898      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34269      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
34269      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35064      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 496.4ns 
35067      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35067      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.4ns 
35068      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37416      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
37417      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38188      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38191      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 561.3ns 
38193      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38194      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.1ns 
38195      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40515      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
40516      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41306      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41309      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 518ns 
41311      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41311      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.9ns 
41312      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43642      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
43643      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44421      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44425      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 984ns 
44429      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44429      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.5ns 
44430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46801      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
46801      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
47545      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
47584      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.96ms 
47586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
47586      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.4ns 
47587      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49967      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
49968      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
50732      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
50793      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 57.93ms 
50800      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
50800      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.7ns 
50801      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53123      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
53123      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
53888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54124      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 226.23ms 
54127      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54128      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.4ns 
54129      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56454      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
56454      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57215      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57220      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ms 
57221      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57221      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.4ns 
57222      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59553      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
59554      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60319      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60322      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
60325      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60325      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.5ns 
60327      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62659      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
62659      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
63398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
63434      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.78ms 
63436      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
63436      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.7ns 
63437      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65800      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
65801      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
66559      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
66574      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.24ms 
66575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
66576      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.1ns 
66576      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68883      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
68883      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
69680      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
69695      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.54ms 
69697      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
69699      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.38ms 
69703      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72030      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
72030      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
72793      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
72807      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.61ms 
72808      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
72808      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109ns 
72809      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75113      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
75113      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
75872      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
75886      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.16ms 
75888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
75888      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.6ns 
75889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78210      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
78211      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
78947      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
78971      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.57ms 
78972      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
78972      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.8ns 
78973      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
81303      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
81303      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
82042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
82045      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
82046      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
82046      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
82047      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
84372      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
84373      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
85139      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
85206      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.79ms 
85208      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
85208      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.1ns 
85209      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87537      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
87538      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
88311      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
88368      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.04ms 
88370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
88370      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.7ns 
88372      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90684      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
90684      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
91439      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
91479      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.99ms 
91481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
91481      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns 
91482      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93794      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
93795      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
94556      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
94563      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.99ms 
94564      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
94565      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns 
94565      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96889      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
96889      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
97627      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
97639      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.51ms 
97640      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
97640      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
97641      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99951      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
99951      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
100705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
100715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ms 
100716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
100716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
100717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
103016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
103793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
103800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.83ms 
103801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
103801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
103802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
106135     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
106895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
106903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
106906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
106906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.5ns 
106907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
109211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
109976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
109982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
109984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
109984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.7ns 
109985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112300     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
112300     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
113034     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
113037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
113039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
113039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
113039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
115367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
116101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
116110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.04ms 
116113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
116113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
116114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
118433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
119191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
119239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.77ms 
119240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
119240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
119241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
121544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
121544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
122298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
122313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.22ms 
122315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
122315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
122316     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
124607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
125363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
125378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.97ms 
125380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
125380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.1ns 
125381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
127687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
128444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
128460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.18ms 
128461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
128461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.3ns 
128462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
130781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
130781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
131515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
131530     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.5ms 
131532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
131532     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.5ns 
131532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
133841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
134594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
134631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.19ms 
134633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
134633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
134633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
136947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
137704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
137707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
137709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
137709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 269.2ns 
137710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
140007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
140007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
140762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
140766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.2ms 
140768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
140768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.6ns 
140769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
143065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
143822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
143829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.37ms 
143830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
143831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
143831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
146149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
146887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
146899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.49ms 
146904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
146904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.6ns 
146905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
149222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
149971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
150011     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.84ms 
150012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
150012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
150013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
152354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
152354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
153105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
153113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
153114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
153114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
153115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
155404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
156154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
156157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
156158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
156158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
156159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
158451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
159211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
159214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
159215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
159215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
159216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
161512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
162263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
162267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
162268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
162268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
162269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
164568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
165299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
165361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.03ms 
165362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
165362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
165363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
167677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
168430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
168498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.18ms 
168501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
168501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.7ns 
168502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
170787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
170787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
171538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
171541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
171542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
171542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
171543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
173831     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
173831     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
174585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
174621     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.35ms 
174625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
174627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.14ms 
174628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
176930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
176930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
177685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
177712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.29ms 
177713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
177713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
177714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
180026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
180026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
180761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
180764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
180765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
180765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
180766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
183074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
183827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
183970     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 131.77ms 
183972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
183972     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
183973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
186276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
186276     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
187030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
187040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.88ms 
187041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
187041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
187042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
189339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
189339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
190100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
190108     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.06ms 
190109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
190110     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.8ns 
190110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
192407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
193156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
193171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.53ms 
193173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
193173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
193173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
195489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
195490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
196222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
196233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.73ms 
196235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
196236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
196236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
198538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
199271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
199274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
199275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
199275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
199276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
201587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
202343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
202347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
202348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
202348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
202349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
204646     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
205400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
205421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.16ms 
205423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
205423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 210.9ns 
205424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
207715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
208476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
208493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.07ms 
208495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
208495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
208496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
210799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
211562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
211577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.18ms 
211578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
211578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
211579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
213891     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
214625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
214628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
214629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
214629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
214630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
216954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
217709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
217714     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.03ms 
217715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
217716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.6ns 
217717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
220013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
220766     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
220771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.43ms 
220772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
220772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
220773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
223076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
223831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
223834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
223835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
223835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.8ns 
223836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
226132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
226132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
226884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
226886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 635.1ns 
226887     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
226887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.9ns 
226888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
229201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
229934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
229937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
229938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
229939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
229939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
232263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
232263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
232996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
232999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 946.2ns 
233000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
233000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
233001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
235325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
236079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
236126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44ms 
236128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
236128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191ns 
236129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
238450     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
239207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
239255     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.34ms 
239257     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
239258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.3ns 
239259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
241573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
242325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
242363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.96ms 
242364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
242364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
242365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
244675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
244675     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
245442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
245492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.49ms 
245493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
245493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
245494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
247822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
247822     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
248557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
248588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.52ms 
248589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
248590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
248590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
250925     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
251687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
251746     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.25ms 
251748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
251748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
251748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
254127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
254881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
254907     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.73ms 
254908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
254908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
254909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
257206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
257964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
257983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ms 
257985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
257985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
257985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
260286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
261036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
261060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.88ms 
261061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
261061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
261062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
263367     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
264097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
264122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.65ms 
264123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
264124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
264125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
266439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
267187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
267214     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.97ms 
267215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
267215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
267216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
269507     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
270267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
270292     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.3ms 
270294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
270294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
270294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
272589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
273355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
273379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.94ms 
273381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
273381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
273382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
275670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
276422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
276446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.17ms 
276447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
276447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
276448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
278754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
278754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
279486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
279506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.27ms 
279507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
279508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
279508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
281814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
282571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
282594     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.88ms 
282595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
282595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.1ns 
282596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
284894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
285646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
285670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.2ms 
285671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
285671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
285672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
287959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
288711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
288718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.23ms 
288719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
288720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
288720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
291012     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
291768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
291785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.28ms 
291786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
291786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
291787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
294097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
294833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
294836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
294838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
294838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
294838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
297187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
297918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
297921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 559.5ns 
297922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
297922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
297922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
300225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
300225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
300995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
300998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 804.8ns 
300999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
300999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
301000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
303301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
303301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
304053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
304059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.39ms 
304061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
304061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
304061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
306342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
307097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
307102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.88ms 
307104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
307104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
307105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
309390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
310146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
310157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.14ms 
310158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
310158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
310159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
312461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
313192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
313196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
313197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
313197     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.6ns 
313197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
315499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
316249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
316251     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 489.9ns 
316252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
316252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
316253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
318534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
319287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
319293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
319294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
319294     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
319294     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
321593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
322344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
322346     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 639.4ns 
322347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
322349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.32ms 
322350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
324635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
325389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
325391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 520.7ns 
325392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
325392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.3ns 
325393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327705     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
327705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
328438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
328440     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 536.8ns 
328441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
328441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
328442     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
330754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
331487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
331491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
331492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
331492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
331492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
333787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
334538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
334546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.32ms 
334547     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
334547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
334548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
336834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
337589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
337592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
337594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
337594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
337594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
339888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
340644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
340651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
340652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
340652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
340652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
342943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
343696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
343700     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.49ms 
343701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
343702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
343702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
346015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
346747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
346762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.26ms 
346763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
346763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
346764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
349077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
349837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
349844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
349846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
349846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.9ns 
349846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352136     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
352136     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
352888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
352891     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
352893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
352893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
352893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
355180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
355180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
355932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
355936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
355937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
355937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.4ns 
355938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
358222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
358977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
358994     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.76ms 
358995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
358995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
358995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
361298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
362057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
362061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 462.3ns 
362062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
362062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
362063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
364375     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
365109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
365145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.3ms 
365147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
365147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
365147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
367461     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
368214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
368217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.54ms 
368219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
368219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.8ns 
368219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
370504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
371256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
371277     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.18ms 
371278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
371278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
371279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
373558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
374308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
374327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.55ms 
374328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
374328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
374329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376644     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
376645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
377382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
377404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.79ms 
377406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
377406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
377406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
379744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
380501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
380504     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 519.1ns 
380505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
380505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.1ns 
380506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
382812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
383570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
383575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.6ms 
383577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
383577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
383577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
385884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
386642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
386645     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
386646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
386646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
386647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
388978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
389720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
389723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 762.7ns 
389724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
389724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
389725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
392040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
392796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
392798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 784.8ns 
392799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
392799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
392800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
395088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
395844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
395847     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
395848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
395848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
395849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
398127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
398886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
398888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
398889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
398889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
398890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
401195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
401932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
401942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.1ms 
401943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
401943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
401944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
404249     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
405009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
405023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.59ms 
405024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
405024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
405025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
407316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
408076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
408088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.33ms 
408089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
408089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
408090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
410409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
411152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
411167     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.58ms 
411169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
411169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
411169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413482     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
413482     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
414252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
414258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.23ms 
414261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
414261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.7ns 
414262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
416578     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
417345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
417350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.85ms 
417351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
417351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
417352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
419681     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
420422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
420424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 778.7ns 
420425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
420425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
420426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
422723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
423489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
423492     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
423493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
423493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
423494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
425801     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
426563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
426565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 881.5ns 
426566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
426566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
426567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
428861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
429619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
429629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.18ms 
429630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
429630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
429631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
431926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
432692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
432697     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
432698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
432698     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.6ns 
432699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
434999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
435739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
435745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.55ms 
435747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
435747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.3ns 
435748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
438073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
438833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
438835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 638.4ns 
438837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
438837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
438837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
441114     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
441874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
441876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 565.2ns 
441877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
441878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.6ns 
441878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
444175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
444932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
444935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
444936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
444936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
444937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
447217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
447977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
447979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
447980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
447980     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
447981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
450277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
451035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
451038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
451039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
451039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.2ns 
451040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453317     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
453317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
454074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
454077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
454078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
454078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
454078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
456377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
457134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
457140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ms 
457141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
457141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
457141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
459422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
460183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
460186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
460187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
460187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
460187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
462494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
463254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
463265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.15ms 
463266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
463266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
463267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
465549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
466307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
466310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608.9ns 
466311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
466311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158ns 
466312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
468612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
469370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
469376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
469377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
469377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
469378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471658     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
471658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
472416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
472418     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 871.5ns 
472419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
472419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
472419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474715     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
474715     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
475473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
475475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 751.9ns 
475476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
475476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
475476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
477757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
477757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
478516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
478520     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
478521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
478521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
478522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
480823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
481584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
481587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
481588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
481588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
481589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
483884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
483884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
484623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
484626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
484628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
484628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
484628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
486924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
487682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
487686     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
487687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
487687     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
487688     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
489996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
489996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
490756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
490761     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.03ms 
490762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
490762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
490763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
493053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
493811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
493825     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.98ms 
493826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
493826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
493827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
496134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
496891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
496906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.73ms 
496907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
496907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
496908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
499203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
499942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
499952     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.98ms 
499953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
499953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
499954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502247     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
502247     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
503005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
503019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.3ms 
503020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
503020     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
503021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
505314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
506072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
506097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.45ms 
506098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
506098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
506099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
508404     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
509176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
509234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 55.93ms 
509235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
509235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
509236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
511527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
512286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
512308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.53ms 
512309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
512310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
512310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
514616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
515376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
515391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.6ms 
515393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
515393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
515393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
517689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
518449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
518477     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.79ms 
518478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
518478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
518479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
520780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
521521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
521566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.48ms 
521567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
521567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.1ns 
521568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
523863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
524621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
524658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.2ms 
524659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
524659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
524660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
526960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
527722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
527762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.69ms 
527763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
527763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
527764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
530067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
530830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
530873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.27ms 
530874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
530874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
530875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533190     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
533190     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
533953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
534068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.58ms 
534069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
534069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
534070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
536382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
537122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
537129     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.69ms 
537131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
537131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
537131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539422     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
539422     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
540181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
540189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.59ms 
540196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
540196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
540196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
542479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
543235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
543241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms 
543242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
543242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
543243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
545534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
546291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
546308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.89ms 
546309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
546309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
546310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
548599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
548599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
549358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
549369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.56ms 
549370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
549370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
549370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
551666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
552424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
552427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
552428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
552429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
552429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
554722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
554722     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
555462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
555479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.35ms 
555480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
555480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
555480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557775     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
557776     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
558536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
558552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.63ms 
558553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
558553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
558554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
560850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
560850     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
561647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
561666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.05ms 
561668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
561668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 167.1ns 
561669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
564056     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
564829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
564832     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
564833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
564833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
564833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
567120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
567878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
567881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.96ms 
567882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
567882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.3ns 
567883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
570179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
570940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
570946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
570947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
570947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.6ns 
570948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573256     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
573256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
574016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
574022     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.32ms 
574023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
574024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.4ns 
574024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
576316     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
577076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
577143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.27ms 
577145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
577145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
577145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
579506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
580266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
580291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.97ms 
580292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
580292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
580293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
582594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
583358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
583380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.19ms 
583381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
583381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
583382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
585683     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
586449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
586451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 296.3ns 
586452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
586453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
586453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
588754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
589513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
589702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 177.32ms 
589703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
589703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107ns 
589704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
592015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
592801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
592849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.86ms 
592850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
592850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
592851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
595223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
595985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
595987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 337.2ns 
595988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
595988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.2ns 
595989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
598295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
599055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
599057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 315.9ns 
599058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
599058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
599059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
601354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
602121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
602123     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 324.4ns 
602124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
602124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.1ns 
602125     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
604441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
605206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
605208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 432.6ns 
605209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
605209     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.2ns 
605210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
607552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
608315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
608421     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.79ms 
608423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
608423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.3ns 
608424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
610773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
611542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
611593     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.59ms 
611594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
611594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
611599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
613908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
613908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
614668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
614669     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.4ns 
614692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
614725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
614741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
614745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
614750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
614753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
614754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
614756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
614758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
614760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
614762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
614763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
614947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
614948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
614949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
614950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
614951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
615050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
615052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
615052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
615054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
615055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
615056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
615212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
615214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
615215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
615215     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
615216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
615217     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
615325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
615326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
615327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
615328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
615329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
615330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
615336     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
615337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
615337     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
615339     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
615340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
615341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
615347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
615348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
615348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
615349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
615350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
615351     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
615477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
615478     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
615479     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
615587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
615589     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)'' 
615592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
615593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
615594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
615595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
615595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
615596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
615604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
615605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
615606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
615607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
615608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
615707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
615711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
615712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
615713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
615714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
615715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
615715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
615821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
615823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
615824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
615825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
615826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
615827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
615827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
615828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
615909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
615910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
616025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
616029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
616033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
616034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
616035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
616036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
616037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
616037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
616038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
616039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
616046     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
616050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
616139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
616140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
616141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
616142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
616143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
616143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
616143     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
616144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
616189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
616194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
616273     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
616275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
616277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
616278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
616279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
616280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
616396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
616400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
616401     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)'' 
616403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
616404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
616404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
616405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
616406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
616414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
616415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
616417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
616417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
616542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
616544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
616545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
616545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
616546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
616547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
616640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
616641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
616642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
616643     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
616644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
616644     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
616645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
616646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
616722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
616724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
616794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
616795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
616795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
616799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
616803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
616807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
616920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
616921     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
616922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
616923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
616932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
617013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
620419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
620420     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)'' 
620426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
620427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
620433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
620434     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
620435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
620442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
620443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
620445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
620445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
620446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
620572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
620576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
620577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
620577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
620578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
620579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
620579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
620667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
620668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
620669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
620670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
620671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
620671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
620672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
620673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
620745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
620746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
620818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
620822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
620826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
620827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
620828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
620829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
620838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
620917     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
620918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
620919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
620919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
620992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
621001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
621003     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)'' 
621005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
621006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
621006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
621007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
621007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
621018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
621019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
621020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
621021     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
621022     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
621110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
621112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
621113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
621114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
621115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
621206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
621210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
621211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
621212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
621213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
621213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
621214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
621312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
621314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
621315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
621316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
621316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
621317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
621317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
621319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
621320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
621320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
621321     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
621322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
621322     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
621323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
621323     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
621407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
621408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
621414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
621488     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
621565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
621567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
621568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
621569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
621569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
621570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
621570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
621571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
621572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
621654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
621660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
621747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
621748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
621749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
621750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
621750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
621751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
621751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
621752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
621757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
621758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
621834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
621839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
621845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
621940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
621941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
621942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
621943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
621944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
621944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
621944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
621945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
621998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
622000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
622000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
622001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
622002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
622007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
622012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
622123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
622246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
622247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
622248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
622249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
622416     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
622500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
622501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
625457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
625463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
625464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
625465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
625466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
625618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
625620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
625621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
625622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
625623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
625722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
628595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
631669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
631674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
631675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
631675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
631676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
631785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
631787     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
631788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
631788     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)' ...' 
631790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
632915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
632916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
632916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
635288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
636072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
636073     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.4ns 
636074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
636079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
636091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
636093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
636095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
636095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
636099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
636101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
636103     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
636106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
636106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
636114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
636115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
636116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
636160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
636161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
636161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
636162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
636162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
636230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
636231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
636232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
636233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
636233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
636236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
636237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
636237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
636238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
636239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
636239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
636327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
636328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
636328     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
636329     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
636330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
636330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
636421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
636422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
636422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
636422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
636423     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
636424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
636424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
636424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
636425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
636425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
636425     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
636426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
636426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
636427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
636427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
636427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
636428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
636428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
636477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
636480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
636518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
636519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
636580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
636581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
636582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
636583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
636585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
636585     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
636630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
636632     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
636634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
636635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
636636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
636637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
636637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
636680     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
636683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
636685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
636731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
636780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
636780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.5ns 
636781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
639154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
639154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
639959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
639989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.8ms