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

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

tests
0

failures
0

ignored
10m34.58s

duration
100%

successful

Tests

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

Standard output

493        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
517        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.43ms 
754        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
771        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)

1721       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1723       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1726       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1727       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3037       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8529       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.77s 
8589       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8621       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.1ns 
8632       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8633       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 186.9ns 
8636       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11352      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
11355      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12269      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12292      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.94ms 
12303      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12303      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.7ns 
12305      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14845      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
14846      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15747      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15761      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.56ms 
15763      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15763      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.7ns 
15765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18255      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
18255      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19063      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19079      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.84ms 
19085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19086      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.2ns 
19087      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21571      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
21572      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22379      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22393      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.45ms 
22397      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22397      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.3ns 
22399      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24787      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
24787      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
25613      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
25652      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.4ms 
25657      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
25657      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.1ns 
25658      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
28055      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
28056      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
28855      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
28875      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.38ms 
28879      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
28880      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 373.1ns 
28881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
31268      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
31268      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
32077      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
32083      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
32086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
32086      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 138ns 
32087      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34492      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
34492      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
35281      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
35284      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 583.9ns 
35286      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
35287      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 603.5ns 
35288      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37663      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
37663      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
38439      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
38441      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 532.8ns 
38442      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
38442      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118ns 
38443      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40811      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
40812      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
41591      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
41594      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 608.4ns 
41596      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
41597      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.2ns 
41598      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
43963      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
43963      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
44736      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
44740      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 987.19ns 
44745      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
44745      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.5ns 
44753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
47219      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
47219      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
48004      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
48096      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 84.18ms 
48101      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
48101      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 161.8ns 
48102      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
50485      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
50485      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
51273      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
51318      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.5ms 
51320      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
51320      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145.1ns 
51326      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53703      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
53703      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
54468      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
54597      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 119.97ms 
54600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
54600      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.6ns 
54601      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56934      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
56934      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
57703      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
57708      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.61ms 
57709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
57709      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
57710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60088      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
60089      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
60929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
60937      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.8ms 
60939      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
60939      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
60940      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63302      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
63303      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
64068      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
64106      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.18ms 
64114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
64114      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 365ns 
64115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66459      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
66460      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
67234      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
67249      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.32ms 
67251      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
67251      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.4ns 
67252      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69610      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
69610      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
70381      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
70397      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.17ms 
70400      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
70400      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 348.4ns 
70405      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72756      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
72756      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
73522      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
73537      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.41ms 
73540      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
73540      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.8ns 
73541      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75970      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
75971      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
76715      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
76736      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.36ms 
76742      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
76743      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.2ns 
76744      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79098      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
79098      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
79866      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
79894      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.66ms 
79896      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
79896      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.5ns 
79897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82240      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
82240      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
83010      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
83013      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 963.29ns 
83014      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
83014      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
83015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85363      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
85363      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
86106      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
86144      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.23ms 
86145      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
86145      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.3ns 
86146      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
88493      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
88493      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
89255      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
89307      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.47ms 
89308      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
89308      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
89309      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91637      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
91637      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
92418      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
92459      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.94ms 
92460      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
92461      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.3ns 
92461      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94814      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
94814      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
95577      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
95584      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
95586      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
95586      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.4ns 
95587      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97917      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
97918      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
98679      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
98690      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.17ms 
98692      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
98692      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
98693      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
101043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
101784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
101797     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.32ms 
101805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
101805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 288.8ns 
101806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
104140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
104916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
104923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.18ms 
104925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
104926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.2ns 
104927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
107284     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
108056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
108065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.9ms 
108067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
108067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.7ns 
108068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
110437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
111201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
111208     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
111209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
111210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
111210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
113531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
114288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
114291     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
114293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
114293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
114293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
116615     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
117373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
117383     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.89ms 
117384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
117385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.3ns 
117386     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
119720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
120480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
120532     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.56ms 
120535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
120535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.9ns 
120536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
122851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
123611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
123628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.53ms 
123629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
123629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
123630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
125977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
126726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
126744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.44ms 
126746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
126747     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.2ns 
126748     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
129085     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
129845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
129862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.84ms 
129863     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
129863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117ns 
129864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132175     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
132175     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
132953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
132969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.73ms 
132971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
132971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101ns 
132972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
135326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
136089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
136133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.41ms 
136142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
136142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 340.1ns 
136148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
138457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
139218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
139221     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 924.69ns 
139223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
139223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 259.1ns 
139224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
141585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
142323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
142327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
142328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
142328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
142329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
144682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
145440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
145447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.6ms 
145449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
145449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
145449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
147777     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
148535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
148543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.07ms 
148545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
148545     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.1ns 
148545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
150869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
151603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
151625     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.51ms 
151627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
151628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 562.7ns 
151629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
153955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
154712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
154719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.53ms 
154720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
154721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
154721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
157027     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
157785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
157788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
157789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
157789     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
157790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
160122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
160876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
160880     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
160881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
160881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
160882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
163193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
163947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
163951     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
163952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
163952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
163953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
166277     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
167012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
167077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.49ms 
167079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
167079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.7ns 
167080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
169419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
170182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
170266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.16ms 
170268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
170268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.9ns 
170269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172576     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
172576     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
173334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
173338     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.62ms 
173340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
173340     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 234.1ns 
173341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
175693     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
176446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
176478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.04ms 
176480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
176480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
176480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
178787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
179543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
179571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.58ms 
179572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
179572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
179573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
181911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
182645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
182647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
182648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
182648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
182649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
184973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
185749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
185931     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 170.61ms 
185933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
185934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.8ns 
185934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
188259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
189015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
189025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.26ms 
189026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
189026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
189027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191352     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
191353     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
192111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
192118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.75ms 
192119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
192119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
192120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
194426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
195181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
195196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.99ms 
195198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
195198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
195198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
197501     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
198258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
198270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.29ms 
198272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
198273     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 229.3ns 
198274     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
200592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
201344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
201348     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
201349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
201349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
201350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
203651     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
204407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
204411     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.5ms 
204412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
204412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
204413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
206737     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
207471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
207494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.66ms 
207495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
207495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
207496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
209826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
210583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
210599     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.57ms 
210600     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
210601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
210601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
212909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
213678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
213693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.13ms 
213694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
213694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
213695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
216030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
216785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
216789     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
216790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
216790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71ns 
216790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
219093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
219093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
219850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
219854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.52ms 
219856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
219856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
219856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
222160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
222160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
222938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
222943     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
222944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
222944     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.1ns 
222945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
225262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
226019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
226021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
226023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
226023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
226023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
228328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
229083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
229085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 619.9ns 
229086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
229086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
229087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
231410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
232144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
232147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
232149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
232149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
232149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
234469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
234469     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
235221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
235223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 931.39ns 
235224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
235224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
235225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
237525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
238278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
238325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.33ms 
238327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
238327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.8ns 
238328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
240649     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
241402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
241445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.28ms 
241447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
241447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.9ns 
241448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
243757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
244512     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
244540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.45ms 
244541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
244541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
244542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
246864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
247597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
247638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.02ms 
247639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
247639     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
247640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
249963     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
250719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
250749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.62ms 
250750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
250750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.6ns 
250751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
253057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
253810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
253860     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.95ms 
253861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
253861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
253862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
256192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
256949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
256975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.97ms 
256976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
256976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
256977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
259287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
260042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
260061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.08ms 
260063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
260063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
260064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
262390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
262390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
263129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
263154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.54ms 
263156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
263157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 385.9ns 
263157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
265489     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
266241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
266261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.51ms 
266262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
266262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
266263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
268567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
269321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
269347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.85ms 
269349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
269349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
269349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271672     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
271672     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
272410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
272439     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.35ms 
272441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
272442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.8ns 
272443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
274759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
274760     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
275514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
275539     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.02ms 
275540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
275540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
275541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
277851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
278608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
278632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.35ms 
278633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
278634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
278634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
280965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
280966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
281718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
281739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.51ms 
281740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
281740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
281741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
284053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
284053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
284810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
284834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.6ms 
284835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
284836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
284836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
287168     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
287902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
287927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.59ms 
287928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
287928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
287929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
290255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
291016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
291024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.36ms 
291026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
291026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199ns 
291027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
293331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
294085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
294102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.68ms 
294103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
294103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
294104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
296426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
297179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
297183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
297185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
297185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172ns 
297186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
299504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
300259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
300261     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 519ns 
300263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
300263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.1ns 
300263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
302593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
303328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
303330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 671.5ns 
303332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
303332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.9ns 
303332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
305652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
306406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
306412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.46ms 
306413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
306413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
306414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
308720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
309477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
309483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.89ms 
309485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
309485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172ns 
309486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
311810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
311811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
312545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
312557     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.69ms 
312558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
312558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
312558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
314903     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
315660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
315664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
315665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
315665     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.7ns 
315666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
317966     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
318720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
318722     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 499.6ns 
318723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
318723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
318724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
321054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
321055     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
321807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
321812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
321814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
321814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
321814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
324117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
324870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
324872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 585.5ns 
324873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
324874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
324874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
327187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
327187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
327922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
327923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 531.8ns 
327925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
327925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
327925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
330240     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
330996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
330998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 559.1ns 
330999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
330999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
331000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
333293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
333293     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
334046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
334049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.81ms 
334050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
334050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
334051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
336362     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
336362     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
337097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
337105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.48ms 
337106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
337106     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62ns 
337107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
339417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
340173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
340178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
340180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
340180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179ns 
340187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
342502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
343255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
343262     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.88ms 
343263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
343263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
343264     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
345577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
346331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
346335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
346336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
346336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.4ns 
346337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
348640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
349393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
349408     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.42ms 
349409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
349409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.4ns 
349410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
351730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
352462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
352465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
352466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
352467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
352467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
354781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
355533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
355536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
355537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
355538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
355538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
357917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
358675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
358679     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
358680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
358680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.4ns 
358680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
361077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
361849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
361866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.51ms 
361867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
361867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
361868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
364210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
364945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
364949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 562.9ns 
364951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
364951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
364952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
367258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
368008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
368048     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.57ms 
368049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
368049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
368050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
370346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
371101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
371105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
371106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
371107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
371107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
373419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
373419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
374171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
374192     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.59ms 
374194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
374194     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
374194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
376486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
377239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
377259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.43ms 
377260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
377260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
377261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
379582     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
380335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
380359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.37ms 
380361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
380361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
380361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
382680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
383414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
383416     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 612.6ns 
383417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
383417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
383418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
385736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
386488     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
386494     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.71ms 
386495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
386495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
386496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
388810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
388810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
389548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
389551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
389552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
389552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
389552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
391867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
391867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
392621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
392623     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 826ns 
392624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
392624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
392625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
394941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
395696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
395698     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822.39ns 
395699     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
395699     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.1ns 
395700     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
398001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
398757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
398760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
398761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
398761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.5ns 
398762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
401081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
401836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
401839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
401840     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
401840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
401841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
404151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
404888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
404896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.69ms 
404897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
404898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
404898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
407211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
407972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
407984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.47ms 
407993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
407993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 159.4ns 
407993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
410310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
411071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
411082     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.21ms 
411083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
411084     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
411084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
413379     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
414141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
414153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.65ms 
414154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
414155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
414155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
416477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
417243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
417248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
417249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
417250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 178.7ns 
417250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
419566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
420326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
420332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
420333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
420333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
420334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
422638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
423405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
423407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.9ns 
423409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
423409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.4ns 
423410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425728     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
425728     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
426497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
426499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
426501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
426501     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
426501     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
428816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
428816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
429577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
429579     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770ns 
429580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
429581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
429581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
431895     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
432649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
432659     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.38ms 
432660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
432660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.3ns 
432661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
434983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
435741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
435745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.35ms 
435746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
435746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
435747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
438052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
438816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
438822     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.51ms 
438824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
438824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206ns 
438825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441130     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
441130     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
441890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
441892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 643.5ns 
441893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
441893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
441893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
444201     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
444943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
444945     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 578.7ns 
444946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
444946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.2ns 
444947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
447256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
448017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
448021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.09ms 
448022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
448022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
448023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450335     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
450335     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
451096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
451099     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
451100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
451100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.8ns 
451100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
453406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
454167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
454169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
454170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
454171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
454171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
456484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
457244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
457247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
457248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
457248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
457248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
459558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
460344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
460349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.68ms 
460350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
460351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
460351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
462645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
463404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
463407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
463408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
463408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
463409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
465720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
466482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
466493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.71ms 
466494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
466494     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
466495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
468815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
469575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
469577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 603.8ns 
469578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
469578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.8ns 
469579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
471897     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
472658     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
472666     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.26ms 
472667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
472667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
472667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
474982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
475742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
475744     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 833.5ns 
475745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
475745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.4ns 
475746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
478053     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
478815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
478817     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 762.89ns 
478818     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
478818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
478819     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
481127     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
481888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
481893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.18ms 
481894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
481894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
481895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
484208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
484969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
484972     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
484973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
484973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
484974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487282     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
487283     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
488044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
488047     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
488048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
488048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
488049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
490360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
491121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
491124     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
491126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
491126     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.5ns 
491126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
493435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
494196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
494203     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.48ms 
494204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
494204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
494205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
496518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
497279     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
497294     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.72ms 
497295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
497295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
497296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
499610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
500371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
500386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.62ms 
500387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
500387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.3ns 
500388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
502697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
503459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
503469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.57ms 
503470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
503470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.1ns 
503471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
505779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
506538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
506549     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.87ms 
506550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
506550     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
506551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
508857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
509618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
509644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.56ms 
509645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
509645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
509646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
511956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
512717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
512742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.89ms 
512744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
512744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
512744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
515051     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
515812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
515836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.32ms 
515837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
515837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
515837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
518150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
518913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
518927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.07ms 
518928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
518928     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.7ns 
518929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
521238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
521999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
522036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.95ms 
522038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
522038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.2ns 
522039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
524351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
525110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
525158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.92ms 
525159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
525159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.6ns 
525160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
527486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
528250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
528288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.46ms 
528289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
528289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.5ns 
528290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530610     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
530610     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
531397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
531441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.36ms 
531443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
531444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.5ns 
531445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
533757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
534519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
534563     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.05ms 
534564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
534564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.2ns 
534565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
536873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
537634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
537755     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 113.15ms 
537757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
537757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
537757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
540072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
540858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
540865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.87ms 
540867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
540867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
540867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
543193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
543953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
543960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
543962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
543962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.2ns 
543963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
546269     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
547029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
547034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.59ms 
547035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
547035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
547036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
549342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
550103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
550121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.65ms 
550122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
550122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
550123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
552432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
553194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
553205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.92ms 
553206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
553206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.7ns 
553207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
555584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
556365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
556368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
556369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
556369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54ns 
556370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558679     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
558679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
559439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
559456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.49ms 
559457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
559457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.3ns 
559458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
561764     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
562526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
562542     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.98ms 
562543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
562543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
562544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
564872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
565633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
565653     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.87ms 
565654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
565654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
565655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
567969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
568731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
568734     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
568735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
568735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.2ns 
568736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
571041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
571041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
571804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
571808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
571809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
571809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
571809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
574133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
574133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
574899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
574905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.26ms 
574907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
574907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
574907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
577215     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
577216     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
577977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
577983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
577984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
577984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 44.3ns 
577985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580315     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
580315     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
581077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
581146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.98ms 
581147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
581147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
581148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
583456     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
584217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
584243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.71ms 
584244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
584244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.1ns 
584244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
586579     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
587341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
587363     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.48ms 
587364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
587364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.4ns 
587364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
589673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
590434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
590436     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 252ns 
590438     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
590438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 163.6ns 
590439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592766     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
592767     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
593526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
593723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 185.9ms 
593725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
593725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.8ns 
593726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
596044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
596810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
596862     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.68ms 
596864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
596864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
596864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
599206     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
599968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
599969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 327.1ns 
599971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
599971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 181ns 
599972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602293     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
602294     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
603054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
603056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 335.3ns 
603057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
603057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
603058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
605381     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
606146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
606148     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 326.9ns 
606149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
606150     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
606150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
608460     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
609245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
609247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 478.7ns 
609248     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
609248     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
609249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
611562     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
612324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
612413     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
612431     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 105.05ms 
612434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
612434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.4ns 
612435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
614796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
614796     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
615562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
615609     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
615610     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.15ms 
615611     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
615611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
615612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
617944     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
618720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
618721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.8ns 
618744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
618775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
618792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
618795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
618800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
618803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
618804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
618806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
618808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
618810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
618812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
618813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
618994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
618996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
618997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
618999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
618999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
619124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
619125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
619128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
619131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
619132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
619133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
619309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
619311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
619312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
619313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
619315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
619317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
619426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
619428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
619429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
619430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
619431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
619431     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
619444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
619445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
619446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
619447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
619449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
619451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
619459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
619460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
619461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
619462     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
619463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
619464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
619578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
619579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
619580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
619688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
619690     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)'' 
619693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
619694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
619695     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
619696     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
619697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
619699     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
619703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
619704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
619705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
619706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
619707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
619807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
619810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
619812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
619813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
619814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
619815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
619816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
619932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
619934     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
619935     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
619936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
619937     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
619938     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
619939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
619941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
620043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
620055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
620163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
620172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
620181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
620183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
620184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
620185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
620186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
620186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
620187     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
620188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
620199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
620207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
620307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
620310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
620312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
620313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
620313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
620314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
620314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
620315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
620359     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
620363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
620439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
620441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
620442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
620444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
620445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
620445     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
620545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
620548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
620551     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)'' 
620553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
620554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
620555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
620556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
620556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
620564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
620572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
620573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
620574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
620650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
620652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
620652     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
620653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
620654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
620655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
620793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
620794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
620795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
620797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
620798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
620798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
620799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
620800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
620872     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
620874     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
620940     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
620941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
620941     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
620945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
620948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
620952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
621062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
621064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
621065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
621067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
621076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
621148     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
624420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
624421     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)'' 
624426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
624427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
624428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
624428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
624429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
624436     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
624437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
624438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
624439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
624439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
624519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
624523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
624524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
624525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
624525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
624526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
624526     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
624608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
624609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
624610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
624611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
624612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
624612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
624613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
624614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
624682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
624683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
624754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
624757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
624761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
624762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
624763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
624764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
624775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
624886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
624887     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
624888     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
624889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
624951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
624959     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
624960     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)'' 
624962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
624963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
624963     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
624964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
624964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
624973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
624975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
624976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
624976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
624977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
625051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
625053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
625054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
625055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
625056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
625133     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
625137     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
625138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
625139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
625139     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
625140     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
625141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
625225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
625226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
625227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
625228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
625229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
625230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
625230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
625231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
625232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
625233     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
625234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
625234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
625234     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
625235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
625235     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
625311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
625312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
625317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
625384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
625453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
625454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
625455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
625455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
625457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
625457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
625457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
625457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
625458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
625532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
625538     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
625615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
625616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
625616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
625617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
625618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
625618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
625618     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
625619     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
625624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
625624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
625694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
625698     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
625703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
625788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
625789     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
625790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
625791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
625791     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
625792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
625792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
625793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
625840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
625842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
625842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
625843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
625844     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
625849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
625853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
625956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
626032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
626033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
626034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
626035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
626180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
626319     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
626320     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
629394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
629399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
629400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
629401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
629402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
629500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
629501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
629502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
629503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
629504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
629594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
632258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
635050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
635055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
635055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
635056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
635057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
635154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
635155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
635156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
635157     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)' ...' 
635158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
636238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
636238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.8ns 
636239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.37s 
638612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
639398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
639400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.5ns 
639400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
639406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
639417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
639420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
639421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
639422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
639426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
639427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
639429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
639432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
639433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
639439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
639441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
639442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
639480     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
639481     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
639482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
639482     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
639483     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
639539     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
639540     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
639541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
639542     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
639543     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
639545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
639546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
639546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
639547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
639548     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
639549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
639622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
639623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
639624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
639625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
639626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
639626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
639702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
639703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
639703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
639704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
639704     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
639705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
639706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
639706     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
639707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
639707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
639708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
639708     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
639709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
639709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
639710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
639710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
639711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
639712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
639713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
639715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
639746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
639748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
639795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
639796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
639798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
639799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
639800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
639800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
639836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
639838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
639839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
639840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
639841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
639842     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
639843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
639878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
639880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
639883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
639975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
640021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
640021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 243.9ns 
640022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.38s 
642398     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
643209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
643240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.06ms

Standard error

ANTLR Tool version 4.12.0 used for code generation does not match the current runtime version 4.13.0
ANTLR Tool version 4.12.0 used for code generation does not match the current runtime version 4.13.0
ANTLR Tool version 4.12.0 used for code generation does not match the current runtime version 4.13.0
ANTLR Tool version 4.12.0 used for code generation does not match the current runtime version 4.13.0