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

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

tests
0

failures
0

ignored
10m28.90s

duration
100%

successful

Tests

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

Standard output

276        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
296        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.02ms 
487        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
503        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)

1390       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1396       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1400       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1400       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2481       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
7198       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.71s 
7272       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
7307       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.8ns 
7320       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
7320       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.1ns 
7325       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
10010      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.68s 
10012      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
10888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
10911      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.53ms 
10923      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
10924      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 384ns 
10925      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13502      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
13502      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
14346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
14360      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.76ms 
14362      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
14362      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.2ns 
14364      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
16849      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
16849      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
17710      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
17727      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.39ms 
17731      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
17732      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.5ns 
17733      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20186      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
20187      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
20961      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
20975      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.34ms 
20979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
20980      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 896.51ns 
20981      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
23383      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
23384      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
24183      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
24224      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.03ms 
24226      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
24226      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 150.3ns 
24235      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
26630      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.39s 
26631      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
27406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
27436      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.69ms 
27447      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
27447      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 589.21ns 
27448      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29863      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
29864      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
30639      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
30643      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 793.91ns 
30651      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
30651      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.3ns 
30652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33061      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.41s 
33061      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
33809      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
33812      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 548.2ns 
33814      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
33814      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.1ns 
33814      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36309      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
36309      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
37082      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
37084      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 513ns 
37086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
37087      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 341.5ns 
37088      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39453      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
39453      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
40219      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
40221      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 592.2ns 
40223      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
40223      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.4ns 
40224      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42552      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
42552      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
43333      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
43341      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
43345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
43345      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.5ns 
43346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45695      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
45695      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
46454      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
46496      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.97ms 
46497      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
46498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.8ns 
46498      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48841      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
48841      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
49609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
49647      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.32ms 
49650      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
49650      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132ns 
49651      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
51981      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
51982      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
52742      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
52903      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 151.55ms 
52907      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
52908      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.9ns 
52909      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55231      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
55231      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
55992      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
55997      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.83ms 
55999      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
55999      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191.3ns 
56000      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58350      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
58351      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
59094      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
59098      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
59103      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
59103      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.6ns 
59104      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
61444      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
61444      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
62200      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
62238      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.7ms 
62239      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
62239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.3ns 
62240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64551      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
64551      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
65307      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
65323      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.33ms 
65324      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
65324      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
65325      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67624      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
67624      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
68380      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
68394      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.38ms 
68395      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
68395      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.9ns 
68396      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70715      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
70715      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
71453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
71468      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.94ms 
71470      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
71470      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309ns 
71471      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73826      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
73826      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
74585      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
74599      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.71ms 
74600      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
74601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
74601      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76917      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
76918      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
77672      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
77696      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.82ms 
77697      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
77698      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.4ns 
77698      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
80005      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
80006      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
80770      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
80773      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
80776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
80776      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 303.1ns 
80777      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83100      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
83101      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
83837      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
83878      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.17ms 
83881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
83881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.9ns 
83882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86208      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
86208      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
86967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
87022      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.03ms 
87025      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
87025      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 319.2ns 
87026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89331      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
89332      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
90090      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
90145      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.59ms 
90150      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
90152      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.81ms 
90154      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92462      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
92462      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
93218      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
93225      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.25ms 
93226      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
93227      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.2ns 
93227      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95545      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
95546      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
96280      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
96292      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.07ms 
96294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
96294      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.7ns 
96294      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98625      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
98625      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
99379      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
99390      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.78ms 
99391      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
99391      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns 
99392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
101696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
102452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
102462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.95ms 
102464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
102464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
102465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
104806     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
105557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
105564     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
105565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
105566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.5ns 
105566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107886     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
107886     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
108622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
108628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.76ms 
108630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
108630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.8ns 
108630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
110946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
110946     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
111696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
111699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
111701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
111701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91ns 
111702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
114006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
114007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
114761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
114780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.1ms 
114782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
114782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.6ns 
114783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
117091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
117091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
117842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
117890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.34ms 
117892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
117892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
117893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
120207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
120937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
120953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.06ms 
120955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
120955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
120955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123285     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
123285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
124044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
124061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.49ms 
124062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
124062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns 
124063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
126355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
126355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
127104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
127121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.73ms 
127122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
127122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
127123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
129409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
130158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
130175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.04ms 
130176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
130176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
130177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
132486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
133224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
133265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.9ms 
133268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
133268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.2ns 
133269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
135594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
136349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
136353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
136354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
136354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.2ns 
136355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
138658     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
139409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
139413     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
139415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
139415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.6ns 
139416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
141749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
142509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
142517     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.34ms 
142519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
142519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.3ns 
142520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
144829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
144829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
145558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
145566     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.97ms 
145567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
145567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
145568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
147877     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
148625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
148644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.17ms 
148645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
148646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
148653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
150948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
151698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
151706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.24ms 
151708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
151708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.2ns 
151708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
154004     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
154004     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
154756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
154759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.16ms 
154760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
154760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.7ns 
154761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
157118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
157900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
157903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
157904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
157904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
157905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
160228     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
160978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
160981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
160982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
160982     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
160983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
163265     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
164015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
164078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.76ms 
164080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
164081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 247.6ns 
164082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
166370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
167120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
167193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.08ms 
167195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
167195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.9ns 
167196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
169506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
169506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
170235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
170238     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
170239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
170239     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
170240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172540     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
172540     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
173289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
173321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.56ms 
173322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
173322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.2ns 
173323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175611     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
175611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
176360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
176387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.6ms 
176388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
176388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
176389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178673     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
178673     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
179426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
179429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
179431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
179431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172ns 
179432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
181736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
182464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
182595     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 120.77ms 
182597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
182597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 140.7ns 
182598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
184909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
185664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
185676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.73ms 
185678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
185678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
185680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
188003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
188750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
188758     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.1ms 
188759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
188759     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
188760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
191047     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
191794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
191809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.15ms 
191810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
191810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
191811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
194123     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
194848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
194859     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.56ms 
194861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
194861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
194862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
197146     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
197892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
197895     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
197896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
197897     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.2ns 
197897     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200183     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
200183     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
200929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
200933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.67ms 
200934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
200935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
200935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
203207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
203207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
203954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
203977     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.68ms 
203978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
203978     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66ns 
203979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
206287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
206287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
207020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
207036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.94ms 
207037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
207037     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
207038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
209343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
210092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
210106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.95ms 
210107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
210107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
210108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
212402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
213150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
213153     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
213154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
213154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
213155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
215449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
215449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
216196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
216200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.62ms 
216201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
216202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
216202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
218502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
218502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
219229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
219234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
219235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
219235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
219236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
221535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
222282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
222285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
222286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
222286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
222287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
224574     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
225323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
225325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 692.8ns 
225326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
225326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
225327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
227618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
228390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
228394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
228395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
228395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
228395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.35s 
230750     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
231479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
231481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 939.01ns 
231483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
231484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 950.71ns 
231485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
233787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
234535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
234575     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.57ms 
234576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
234577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 189.7ns 
234577     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
236892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
236893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
237641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
237675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.79ms 
237677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
237677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
237678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239969     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
239969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
240722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
240751     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.42ms 
240753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
240753     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202ns 
240754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
243062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
243795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
243837     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.88ms 
243838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
243838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
243839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
246157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
246904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
246932     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.46ms 
246934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
246934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
246934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
249234     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
249983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
250034     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.6ms 
250035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
250035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
250036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
252329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
252329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
253078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
253103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.86ms 
253104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
253104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.8ns 
253105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
255411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
255411     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
256138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
256157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.22ms 
256158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
256158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68ns 
256159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
258464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
258464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
259211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
259237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.29ms 
259240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
259240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.01ns 
259241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
261572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
262318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
262337     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.97ms 
262338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
262339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
262339     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
264618     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
265367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
265394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.42ms 
265395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
265395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
265396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
267694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
267695     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
268421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
268445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.88ms 
268446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
268447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
268447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
270748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
270748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
271495     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
271519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.61ms 
271520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
271520     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
271521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
273827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
274572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
274596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.61ms 
274597     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
274597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
274598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
276879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
277633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
277654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.52ms 
277656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
277656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.2ns 
277657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
279956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
280705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
280729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.22ms 
280731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
280731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
280731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283009     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
283009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
283755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
283780     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.22ms 
283781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
283781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
283782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
286058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
286804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
286812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.54ms 
286813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
286813     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.3ns 
286814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
289108     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
289834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
289850     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.33ms 
289851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
289852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.8ns 
289852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
292154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
292903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
292906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
292907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
292907     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
292908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
295185     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
295185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
295932     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
295934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 549.21ns 
295935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
295935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
295936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
298214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
298961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
298963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 715.51ns 
298964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
298964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
298965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
301259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
301986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
301992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.62ms 
301993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
301993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
301994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
304291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
305040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
305046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.92ms 
305047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
305047     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
305048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
307325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
307325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
308074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
308085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.32ms 
308086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
308086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.5ns 
308087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
310364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
311117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
311120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
311121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
311121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.2ns 
311121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
313396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
314143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
314145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 511.11ns 
314146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
314146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
314147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
316441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
316441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
317170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
317176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.58ms 
317177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
317177     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.1ns 
317177     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
319481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
320232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
320234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 645.91ns 
320235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
320235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
320236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
322538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
323287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
323289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 541.51ns 
323290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
323290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
323291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
325573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
326319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
326321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 572.61ns 
326322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
326322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.9ns 
326323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
328634     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
329368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
329371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.82ms 
329372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
329373     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.4ns 
329373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331684     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
331684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
332433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
332441     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.69ms 
332443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
332443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.7ns 
332443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
334732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
335480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
335483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
335485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
335485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
335485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
337770     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
337770     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
338519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
338526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.89ms 
338527     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
338527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.8ns 
338528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
340832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
340832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
341561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
341565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.53ms 
341566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
341566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
341567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
343869     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
343869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
344619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
344634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.67ms 
344636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
344636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
344636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346922     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
346922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
347670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
347674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
347675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
347675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
347675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
349958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
350708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
350711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
350712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
350712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.2ns 
350713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
353013     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
353742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
353745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
353746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
353746     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.6ns 
353747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
356045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
356792     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
356809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.45ms 
356810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
356810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
356811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
359093     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
359093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
359842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
359846     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 547.41ns 
359848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
359848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
359848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
362141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
362870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
362908     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.69ms 
362909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
362909     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52ns 
362910     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365207     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
365207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
365956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
365959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
365960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
365960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
365961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
368244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
368995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
369016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.57ms 
369018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
369018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
369019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371299     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
371318     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
372047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
372069     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.81ms 
372071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
372071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.1ns 
372072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
374401     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
375149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
375178     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.5ms 
375180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
375180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
375180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
377480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
378234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
378237     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 587.41ns 
378240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
378240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204.1ns 
378241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
380541     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
381269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
381274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.73ms 
381276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
381276     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.5ns 
381276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
383569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
384322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
384325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
384326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
384326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.9ns 
384326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
386609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
387362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
387364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 659.71ns 
387365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
387365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 43.4ns 
387366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
389664     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
390396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
390398     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 771.21ns 
390399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
390399     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.1ns 
390400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
392718     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
393472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
393475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
393476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
393476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.9ns 
393477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
395753     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
396508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
396511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
396513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
396513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 174.6ns 
396514     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
398817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
399568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
399578     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.88ms 
399579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
399579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46.3ns 
399580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
401864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
402618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
402631     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.4ms 
402632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
402632     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
402633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
404929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
404930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
405681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
405693     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.18ms 
405695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
405695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169ns 
405696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
407977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
408738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
408750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.47ms 
408752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
408752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.2ns 
408753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
411050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
411790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
411795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.27ms 
411796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
411796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
411797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414091     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
414091     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
414850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
414856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.12ms 
414857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
414857     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.1ns 
414858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
417155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
417155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
417895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
417897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.61ns 
417898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
417898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.8ns 
417899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
420193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
420951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
420954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.5ms 
420955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
420955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
420956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
423252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
423253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
423995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
423997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
423998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
423998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
423999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426302     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
426302     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
427060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
427071     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.54ms 
427072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
427072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
427073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
429369     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
430109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
430113     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
430114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
430114     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
430115     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
432408     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
433168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
433175     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.67ms 
433176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
433176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
433176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
435475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
436215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
436217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 683.21ns 
436218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
436218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
436219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
438514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
439272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
439274     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 610.21ns 
439275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
439275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
439276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
441577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
441577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
442337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
442341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.17ms 
442342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
442342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
442342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
444624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
444624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
445384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
445387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
445389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
445389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169.2ns 
445390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
447690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
448448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
448451     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.35ms 
448452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
448452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.6ns 
448453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
450743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
451482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
451484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
451485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
451485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
451486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
453788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
454546     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
454551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.52ms 
454552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
454552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.2ns 
454553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
456856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
456856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
457613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
457615     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.32ms 
457616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
457616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
457617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
459892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.27s 
459892     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
460648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
460658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.08ms 
460659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
460659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
460660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
462952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
463709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
463711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.21ns 
463712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
463712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
463713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
466000     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
466757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
466764     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.96ms 
466765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
466765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
466765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
469043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
469801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
469805     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 844.21ns 
469807     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
469807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 46ns 
469808     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
472102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
472102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
472861     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
472863     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 788.71ns 
472864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
472864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
472865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
475172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
475933     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
475938     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.2ms 
475939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
475939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.2ns 
475939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
478222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
478980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
478983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
478984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
478984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
478985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
481278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
482033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
482038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
482040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
482040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.5ns 
482041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
484336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
485094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
485098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.21ms 
485099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
485099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.8ns 
485100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
487396     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
488139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
488144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.23ms 
488145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
488145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
488145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
490451     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
491210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
491224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.21ms 
491225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
491225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
491226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
493523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
493524     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
494282     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
494297     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.15ms 
494298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
494298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
494298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
496592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
496592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
497352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
497362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.51ms 
497363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
497363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.5ns 
497363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
499656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
499656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
500414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
500425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.76ms 
500426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
500426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.4ns 
500426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
502714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
503453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
503478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.21ms 
503479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
503479     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
503480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505774     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
505774     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
506536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
506561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.69ms 
506562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
506562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.9ns 
506562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
508854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
508855     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
509614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
509637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.04ms 
509638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
509638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.7ns 
509639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
511931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
512693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
512707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.97ms 
512708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
512708     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
512709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
514998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
514999     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
515755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
515786     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.21ms 
515787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
515787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.5ns 
515787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
518076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
518076     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
518836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
518882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.81ms 
518883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
518883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
518884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
521181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
521181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
521941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
521978     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.02ms 
521979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
521979     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
521980     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524337     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.36s 
524337     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
525096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
525137     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.12ms 
525138     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
525138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.9ns 
525139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
527436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
528196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
528239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.19ms 
528240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
528240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47ns 
528241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
530537     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
531277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
531419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.68ms 
531420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
531420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
531421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
533713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
534474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
534481     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.79ms 
534483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
534484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.3ns 
534484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
536781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
537544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
537555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.61ms 
537556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
537556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.5ns 
537556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
539853     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
540602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
540607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.55ms 
540608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
540608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.9ns 
540608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
542920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
543659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
543676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.37ms 
543677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
543677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.7ns 
543678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
545988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
545988     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
546728     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
546741     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.41ms 
546743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
546743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.1ns 
546743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
549050     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
549791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
549795     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
549796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
549796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
549796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552108     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
552109     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
552850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
552893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.12ms 
552895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
552895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 180.2ns 
552896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
555188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
555947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
555963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.7ms 
555964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
555964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
555965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
558259     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
558259     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
559019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
559038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.02ms 
559039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
559039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
559040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
561325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
562084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
562087     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
562088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
562088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
562088     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
564382     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
565142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
565145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
565146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
565147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
565147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
567439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
568199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
568205     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ms 
568206     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
568206     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
568207     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
570502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
570503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
571263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
571275     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.94ms 
571277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
571277     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 193.9ns 
571278     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
573605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
573605     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
574364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
574432     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.05ms 
574433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
574433     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.3ns 
574434     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
576744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
577507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
577534     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.43ms 
577535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
577535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.7ns 
577535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
579832     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
580594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
580619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.34ms 
580621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
580621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 214.1ns 
580622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
582934     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
583693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
583695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 318.2ns 
583696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
583696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.4ns 
583697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
585992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
586751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
586947     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 184.68ms 
586949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
586949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.2ns 
586950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.3s 
589255     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
590017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
590066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.51ms 
590067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
590067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.1ns 
590068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
592355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
593116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
593118     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 344.4ns 
593119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
593119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.5ns 
593120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.31s 
595426     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
596185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
596186     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 309.2ns 
596187     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
596187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
596188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
598474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
599233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
599234     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 326.8ns 
599236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
599236     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 47.7ns 
599236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.29s 
601522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
602280     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
602282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 438.7ns 
602283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
602283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.9ns 
602284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604569     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.28s 
604569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
605330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
605412     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
605425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 93.4ms 
605427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
605428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 179.1ns 
605429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
607763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.33s 
607763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
608526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
608573     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
608574     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.48ms 
608575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
608575     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 48.8ns 
608576     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
610892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.32s 
610893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
611656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
611657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.9ns 
611681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
611726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
611742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
611746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
611751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
611754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
611754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
611756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
611759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
611761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
611763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
611764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
611947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
611948     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
611950     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
611951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
611952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
612073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
612074     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
612077     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
612079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
612080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
612081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
612237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
612239     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
612241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
612242     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
612243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
612246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
612380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
612381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
612382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
612383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
612384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
612384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
612392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
612393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
612393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
612395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
612396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
612397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
612404     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
612405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
612406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
612406     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
612407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
612408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
612558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
612559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
612560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
612707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
612709     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)'' 
612711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
612712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
612713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
612714     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
612715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
612715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
612719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
612721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
612722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
612723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
612724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
612847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
612851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
612852     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
612853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
612854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
612855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
612856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
612973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
612975     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
612976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
612977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
612978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
612979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
612979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
612980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
613068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
613069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
613185     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
613188     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
613192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
613193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
613194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
613195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
613195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
613195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
613196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
613197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
613203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
613207     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
613291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
613292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
613292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
613293     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
613294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
613294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
613294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
613295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
613340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
613344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
613424     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
613426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
613427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
613429     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
613430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
613430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
613550     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
613554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
613555     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)'' 
613556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
613557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
613558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
613559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
613559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
613566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
613567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
613569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
613569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
613647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
613648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
613649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
613650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
613650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
613651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
613740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
613741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
613742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
613743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
613744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
613744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
613745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
613746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
613820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
613821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
613889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
613890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
613890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
613894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
613897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
613901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
614007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
614008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
614009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
614010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
614019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
614093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
617361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
617362     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)'' 
617367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
617368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
617369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
617369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
617370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
617377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
617378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
617379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
617380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
617381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
617467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
617470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
617472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
617472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
617473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
617474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
617474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
617562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
617564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
617564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
617566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
617566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
617567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
617567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
617568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
617640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
617642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
617719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
617723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
617727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
617728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
617728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
617729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
617739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
617821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
617822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
617823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
617824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
617893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
617901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
617902     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)'' 
617904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
617905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
617905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
617906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
617906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
617916     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
617918     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
617919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
617919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
617920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
618002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
618003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
618005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
618005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
618006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
618091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
618095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
618096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
618097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
618098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
618098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
618099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
618191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
618193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
618194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
618195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
618196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
618196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
618197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
618198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
618199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
618199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
618200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
618201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
618202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
618202     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
618203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
618284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
618285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
618290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
618363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
618438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
618439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
618440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
618441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
618442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
618442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
618443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
618443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
618444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
618563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
618569     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
618651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
618653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
618653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
618654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
618655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
618655     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
618656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
618656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
618661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
618662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
618734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
618739     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
618744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
618836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
618837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
618838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
618839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
618839     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
618840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
618840     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
618841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
618891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
618891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
618892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
618893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
618893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
618898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
618902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
619010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
619092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
619093     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
619094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
619094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
619249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
619330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
619331     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
622146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
622151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
622152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
622153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
622154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
622260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
622261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
622262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
622263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
622264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
622361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
625117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
628060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
628064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
628065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
628066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
628067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
628172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
628174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
628175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
628176     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)' ...' 
628177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
629244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
629244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.7ns 
629245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.34s 
631585     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
632368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
632369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.8ns 
632370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
632375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
632386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
632389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
632391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
632391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
632395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
632396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
632398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
632401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
632401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
632409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
632410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
632411     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
632451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
632452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
632453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
632453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
632454     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
632509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
632509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
632511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
632512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
632513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
632516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
632516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
632517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
632518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
632519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
632519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
632590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
632590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
632591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
632592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
632593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
632593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
632667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
632668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
632668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
632669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
632669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
632670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
632671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
632671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
632672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
632672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
632673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
632673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
632674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
632674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
632675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
632675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
632676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
632677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
632677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
632679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
632709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
632710     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
632753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
632754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
632756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
632757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
632758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
632759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
632797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
632799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
632800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
632801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
632802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
632803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
632804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
632841     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
632891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
632894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
632939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
632986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
632986     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.8ns 
632987     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.4s 
635392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
636200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
636231     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.74ms