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

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

tests
0

failures
0

ignored
11m9.90s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.240s passed
powPositiveConcrete data()[101] 3.239s passed
powGeq1Concrete data()[102] 3.239s passed
pow2InIntLower data()[103] 3.239s passed
pow2InIntUpper data()[104] 3.241s passed
logSelfConcrete data()[105] 3.242s passed
log1Concrete data()[106] 3.238s passed
logProduct data()[107] 3.248s passed
logTimesBaseConcrete data()[108] 3.242s passed
logProdIdentity data()[109] 3.249s passed
moduloByteIsInByte data()[10] 3.354s passed
logProdIdentityConcrete data()[110] 3.249s passed
logPowIdentity data()[111] 3.240s passed
logPowIdentityConcrete data()[112] 3.240s passed
logPositive data()[113] 3.254s passed
logPositiveConcrete data()[114] 3.246s passed
logMono data()[115] 3.269s passed
logMonoConcrete data()[116] 3.236s passed
powLogLess data()[117] 3.257s passed
powLogMore2 data()[118] 3.261s passed
logLessThanPow data()[119] 3.270s passed
moduloCharIsInChar data()[11] 3.310s passed
logLessThanPowConcrete data()[120] 3.233s passed
logSqueeze data()[121] 3.243s passed
ifthenelse_equals data()[122] 3.237s passed
ifthenelse_equals_1 data()[123] 3.239s passed
ifthenelse_equals_2 data()[124] 3.249s passed
disjointWithSingleton1 data()[125] 3.246s passed
disjointWithSingleton2 data()[126] 3.248s passed
disjointArrayRanges data()[127] 3.272s passed
disjointArrayRangeAllFields1 data()[128] 3.258s passed
disjointArrayRangeAllFields2 data()[129] 3.260s passed
div_unique1 data()[12] 3.350s passed
seqSelfDefinition data()[130] 3.254s passed
seqOutsideValue data()[131] 3.246s passed
castedGetAny data()[132] 3.251s passed
seqGetAlphaCast data()[133] 3.267s passed
getOfSeqSingleton data()[134] 3.265s passed
getOfSeqSingletonConcrete data()[135] 3.246s passed
getOfSeqConcat data()[136] 3.270s passed
getOfSeqSub data()[137] 3.266s passed
getOfSeqReverse data()[138] 3.255s passed
lenOfSeqEmpty data()[139] 3.253s passed
div_unique2 data()[13] 3.374s passed
lenOfSeqSingleton data()[140] 3.243s passed
lenOfSeqConcat data()[141] 3.252s passed
lenOfSeqSub data()[142] 3.242s passed
lenOfSeqReverse data()[143] 3.247s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.268s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.253s passed
getOfSeqSingletonEQ data()[146] 3.247s passed
getOfSeqConcatEQ data()[147] 3.262s passed
getOfSeqSubEQ data()[148] 3.249s passed
getOfSeqReverseEQ data()[149] 3.241s passed
div_exists data()[14] 3.481s passed
lenOfSeqEmptyEQ data()[150] 3.260s passed
lenOfSeqSingletonEQ data()[151] 3.246s passed
lenOfSeqConcatEQ data()[152] 3.250s passed
lenOfSeqSubEQ data()[153] 3.254s passed
lenOfSeqReverseEQ data()[154] 3.280s passed
getOfSeqDefEQ data()[155] 3.248s passed
lenOfSeqDefEQ data()[156] 3.246s passed
seqConcatWithSeqEmpty1 data()[157] 3.263s passed
seqConcatWithSeqEmpty2 data()[158] 3.292s passed
seqReverseOfSeqEmpty data()[159] 3.269s passed
div_one data()[15] 3.312s passed
subSeqComplete data()[160] 3.257s passed
subSeqTailR data()[161] 3.266s passed
subSeqTailL data()[162] 3.285s passed
subSeqTailEQR data()[163] 3.265s passed
subSeqTailEQL data()[164] 3.259s passed
seqDef_split data()[165] 3.296s passed
seqDef_induction_upper data()[166] 3.287s passed
seqDef_induction_upper_concrete data()[167] 3.306s passed
seqDef_induction_lower data()[168] 3.297s passed
seqDef_induction_lower_concrete data()[169] 3.285s passed
jdiv_one data()[16] 3.297s passed
seqDef_split_in_three data()[170] 3.381s passed
seqDef_empty data()[171] 3.254s passed
seqDef_one_summand data()[172] 3.265s passed
seqDef_lower_equals_upper data()[173] 3.253s passed
seqDefOfSeq data()[174] 3.280s passed
seqSelfDefinitionEQ2 data()[175] 3.267s passed
indexOfSeqSingleton data()[176] 3.249s passed
indexOfSeqConcatFirst data()[177] 3.284s passed
indexOfSeqConcatSecond data()[178] 3.263s passed
indexOfSeqSub data()[179] 3.286s passed
div_zero data()[17] 3.324s passed
lenOfArray2seq data()[180] 3.249s passed
getAnyOfArray2seq data()[181] 3.261s passed
getOfArray2seq data()[182] 3.242s passed
getAnyOfNPermInv data()[183] 3.275s passed
seqNPermRange data()[184] 3.335s passed
seqPermTrans data()[185] 3.282s passed
seqPermRefl data()[186] 3.291s passed
seqPermSplit data()[187] 3.241s passed
seqNPermRight data()[188] 3.485s passed
seqPermFromSwap data()[189] 3.331s passed
divResZero1 data()[18] 3.321s passed
seqPermTransAlt0 data()[190] 3.246s passed
seqPermTransAlt1 data()[191] 3.252s passed
seqPermTransAlt2 data()[192] 3.239s passed
seqPermTransAlt3 data()[193] 3.254s passed
seqPermForall data()[194] 3.344s passed
seqPermExists data()[195] 3.302s passed
schiffl_lemma_2 data()[196] 21.891s passed
schiffl_thm_1 data()[197] 3.997s passed
eqSameSeq data()[198] 3.323s passed
divResZero2 data()[19] 3.315s passed
eqTermCut data()[1] 4.089s passed
divResOne1 data()[20] 3.294s passed
divResOne2 data()[21] 3.303s passed
div_cancel1 data()[22] 3.295s passed
div_cancel2 data()[23] 3.280s passed
divAddMultDenom data()[24] 3.305s passed
divMinus data()[25] 3.353s passed
divMinusDenom data()[26] 3.312s passed
divLeastDPos data()[27] 3.291s passed
divLeastDNeg data()[28] 3.293s passed
divGreatestDPos data()[29] 3.275s passed
equivAllRight data()[2] 3.670s passed
divGreatestDNeg data()[30] 3.274s passed
divIncreasingPos data()[31] 3.274s passed
divIncreasingNeg data()[32] 3.271s passed
jdiv_zero data()[33] 3.278s passed
jdivPulloutMinusNum data()[34] 3.293s passed
jdivPulloutMinusDenom data()[35] 3.317s passed
jdiv_uniquePosPos data()[36] 3.289s passed
jdiv_uniquePosNeg data()[37] 3.302s passed
jdiv_uniqueNegPos data()[38] 3.270s passed
jdiv_uniqueNegNeg data()[39] 3.291s passed
irrflConcrete1 data()[3] 3.603s passed
jdivMultDenom1 data()[40] 3.291s passed
jdivMultDenom2 data()[41] 3.263s passed
mod_geZero data()[42] 3.255s passed
mod_lessDenom data()[43] 3.292s passed
jmod_NumPos data()[44] 3.266s passed
jmod_NumNeg data()[45] 3.271s passed
jmod_geZero data()[46] 3.264s passed
jmodNumZero data()[47] 3.271s passed
jmod_pulloutminusNum data()[48] 3.282s passed
jmod_pulloutminusDenom data()[49] 3.247s passed
irrflConcrete2 data()[4] 3.469s passed
jmodUnique1 data()[50] 3.315s passed
jmodUnique2 data()[51] 3.359s passed
intDivRem data()[52] 3.261s passed
jmodjmod data()[53] 3.283s passed
jmodDivisible data()[54] 3.317s passed
jmodDivisibleRep data()[55] 3.276s passed
jdivAddMultDenom data()[56] 3.393s passed
jmodAltZero data()[57] 3.261s passed
jmodAddMultDenomZero data()[58] 3.259s passed
polyDiv_zero data()[59] 3.253s passed
cancel_gtPos data()[5] 3.415s passed
polyMod_ltdivDenom data()[60] 3.254s passed
bsum_empty data()[61] 3.251s passed
bsum_induction_upper data()[62] 3.244s passed
bsum_induction_lower data()[63] 3.260s passed
bsum_num_of_bounds data()[64] 3.273s passed
bsum_num_of_bounds2 data()[65] 3.259s passed
bsum_induction_upper2 data()[66] 3.255s passed
bsum_induction_upper_concrete data()[67] 3.267s passed
bsum_induction_upper_concrete_2 data()[68] 3.239s passed
bsum_induction_upper2_concrete data()[69] 3.251s passed
cancel_gtNeg data()[6] 3.427s passed
bsum_induction_lower_concrete data()[70] 3.244s passed
bsum_induction_lower2 data()[71] 3.250s passed
bsum_induction_lower2_concrete data()[72] 3.251s passed
bsum_positive data()[73] 3.294s passed
bsum_upper_bound data()[74] 3.280s passed
bsum_lower_bound data()[75] 3.295s passed
bsum_positive_lower_bound_element data()[76] 3.287s passed
bsum_sub_same_index data()[77] 3.274s passed
bsum_less_same_index data()[78] 3.303s passed
bsum_equal_except_one_index data()[79] 3.293s passed
moduloIntIsInInt data()[7] 3.399s passed
bsum_num_of_is_max data()[80] 3.283s passed
bsum_num_of_is_max2 data()[81] 3.274s passed
bsum_num_of_is_max3 data()[82] 3.293s passed
bsum_num_of_is_max4 data()[83] 3.285s passed
bsum_num_of_lt_max data()[84] 3.267s passed
bsum_num_of_lt_max2 data()[85] 3.271s passed
bsum_num_of_lt_max3 data()[86] 3.273s passed
bsum_num_of_lt_max4 data()[87] 3.279s passed
bsum_num_of_gt0 data()[88] 3.264s passed
bsum_num_of_gt0_alt data()[89] 3.265s passed
moduloLongIsInLong data()[8] 3.359s passed
bsum_add_concrete data()[90] 3.275s passed
bprod_all_positive data()[91] 3.266s passed
bprod_split data()[92] 3.245s passed
powConcrete0 data()[93] 3.258s passed
powConcrete1 data()[94] 3.246s passed
powSplitFactor data()[95] 3.254s passed
powAdd data()[96] 3.248s passed
powMono data()[97] 3.261s passed
powMonoConcrete data()[98] 3.237s passed
powMonoConcreteRight data()[99] 3.237s passed
moduloShortIsInShort data()[9] 3.349s passed

Standard output

317        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
343        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.54ms 
582        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599        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)

1538       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1541       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1545       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1545       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2940       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8429       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.85s 
8525       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8566       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.6ns 
8583       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8583       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 541.31ns 
8590       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11516      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
11518      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12632      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12661      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.45ms 
12676      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12676      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 411.31ns 
12678      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15408      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
15409      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
16329      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
16343      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.82ms 
16346      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
16346      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 145ns 
16347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
19070      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
19071      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19940      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19947      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.34ms 
19950      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19950      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.4ns 
19951      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22588      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.64s 
22588      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
23410      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
23416      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
23418      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
23419      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 525.11ns 
23420      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25972      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
25973      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26788      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26830      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.24ms 
26834      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26834      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 382.71ns 
26835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29397      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
29397      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
30211      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
30259      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.97ms 
30262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
30262      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.7ns 
30263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32834      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
32835      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33659      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 601.01ns 
33661      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33661      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.6ns 
33663      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
36200      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
36201      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
37015      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
37018      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 565.11ns 
37020      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
37021      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 360.2ns 
37022      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39570      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
39570      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
40364      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
40367      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 651.01ns 
40370      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
40370      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.6ns 
40371      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42927      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
42928      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43718      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43721      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.21ns 
43723      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43724      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.1ns 
43725      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
46235      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
46235      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
47027      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
47030      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 584.91ns 
47038      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
47038      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 372.11ns 
47040      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49552      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
49553      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
50342      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
50381      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.6ms 
50383      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
50383      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.7ns 
50384      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52931      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.55s 
52932      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53720      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
53754      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.63ms 
53758      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
53758      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 364.61ns 
53759      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56254      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
56254      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
57051      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
57235      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 174.65ms 
57238      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
57239      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 422.81ns 
57240      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59754      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
59755      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
60543      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
60548      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.02ms 
60549      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
60549      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.6ns 
60550      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63045      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
63047      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
63841      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
63845      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
63848      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
63849      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.6ns 
63850      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66344      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
66345      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
67132      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
67170      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.59ms 
67171      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
67171      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129ns 
67172      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69674      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
69675      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
70475      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
70490      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.4ms 
70493      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
70493      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.2ns 
70494      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
73006      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
73006      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
73793      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
73806      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.24ms 
73808      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
73808      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.4ns 
73809      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
76296      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
76296      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
77084      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
77100      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.45ms 
77102      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
77103      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.8ns 
77104      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
79601      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
80388      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
80403      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.9ms 
80406      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
80406      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.6ns 
80407      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82887      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
82888      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
83673      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
83698      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.06ms 
83701      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
83701      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 324.9ns 
83702      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86189      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
86190      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
86974      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
86978      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.05ms 
86980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
86980      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 295.5ns 
86981      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89458      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
89459      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
90244      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
90283      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.8ms 
90284      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
90285      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.1ns 
90286      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92781      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
92781      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
93571      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
93636      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 58.5ms 
93639      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
93639      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 336.2ns 
93640      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96121      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
96121      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
96904      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
96949      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.69ms 
96950      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
96950      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.8ns 
96951      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99430      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
99431      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
100219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
100239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.58ms 
100241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
100241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.5ns 
100242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
102735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
103517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
103531     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.01ms 
103533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
103533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.1ns 
103534     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
106007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
106008     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
106793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
106806     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.57ms 
106809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
106809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322.4ns 
106810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
109291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
110073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
110081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.64ms 
110083     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
110083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.41ns 
110084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
112565     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
113347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
113355     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.3ms 
113357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
113357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 224.5ns 
113358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
115833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
116619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
116626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.21ms 
116628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
116628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.8ns 
116629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
119118     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
119899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
119904     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
119906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
119906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 312.2ns 
119908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
122397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
123182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
123196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.56ms 
123199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
123199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.81ns 
123201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
125677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
126456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
126514     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.72ms 
126517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
126517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.5ns 
126518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129005     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
129005     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
129786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
129804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.35ms 
129805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
129805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
129806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132280     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
132280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
133074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
133105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.72ms 
133109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
133109     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 362.9ns 
133110     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
135577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
136357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
136375     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.99ms 
136377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
136377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.8ns 
136378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
138871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
139649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
139667     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
139668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
139668     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.8ns 
139669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
142139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
142918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
142957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.51ms 
142959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
142959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183ns 
142960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145434     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
145435     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
146217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
146220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
146222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
146222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 154.3ns 
146223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
148691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
149471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
149476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
149477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
149478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185ns 
149478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
151977     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
152758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
152767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.31ms 
152768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
152769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 158.7ns 
152769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
155244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
156024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
156033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.38ms 
156035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
156035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.8ns 
156035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
158504     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
159283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
159304     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.23ms 
159305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
159305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.4ns 
159306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
161781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
162560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
162568     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.14ms 
162570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
162570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.5ns 
162571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
165044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
165044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
165835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
165839     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
165841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
165841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 169ns 
165842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
168336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
169118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
169122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
169123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
169123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
169124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171585     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
171586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
172364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
172368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
172369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
172369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
172370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
174836     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
175614     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
175683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 59.71ms 
175685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
175685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.4ns 
175686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
178181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
178963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
179042     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.62ms 
179044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
179044     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 191ns 
179045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
181518     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
182297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
182303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms 
182305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
182306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.7ns 
182307     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184773     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
184773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
185551     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
185585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.74ms 
185588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
185588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.3ns 
185589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
188085     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
188086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
188864     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
188902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.81ms 
188905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
188906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 292.4ns 
188907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191394     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
191395     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
192176     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
192179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
192181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
192182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.1ns 
192183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
194656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
195432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
195572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 128.03ms 
195574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
195574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.5ns 
195575     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
198045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
198821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
198833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.15ms 
198834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
198834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.1ns 
198835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
201308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
202084     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
202093     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.38ms 
202094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
202094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
202095     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
204552     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
205328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
205345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.81ms 
205346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
205347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.6ns 
205347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207808     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
207808     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
208584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
208598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.11ms 
208602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
208602     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266ns 
208603     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
211071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
211071     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
211847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
211851     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
211853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
211853     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.9ns 
211854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
214314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
215091     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
215096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.84ms 
215097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
215097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.8ns 
215098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
217558     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
218333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
218356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.34ms 
218358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
218359     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 300.4ns 
218361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220834     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
220834     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
221613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
221629     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.75ms 
221631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
221631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
221632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
224097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
224873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
224889     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.15ms 
224890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
224890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
224891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
227363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
228139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
228143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
228144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
228144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
228145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
230630     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
231406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
231410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.65ms 
231411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
231411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.4ns 
231412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
233869     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
234644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
234649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.63ms 
234650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
234651     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.1ns 
234651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
237122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
237898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
237901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
237902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
237902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
237903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
240361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
241141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
241144     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 782.41ns 
241147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
241147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.6ns 
241148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243614     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
243614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
244391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
244395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.28ms 
244396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
244396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 
244397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
246864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
247644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
247646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.07ms 
247648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
247648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
247649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
250120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
250895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
250940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.11ms 
250941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
250941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.3ns 
250942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
253410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
254185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
254220     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.58ms 
254222     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
254222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.4ns 
254223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
256697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
257477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
257515     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.23ms 
257518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
257518     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 322ns 
257519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
259985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
259985     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
260760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
260802     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 38.22ms 
260804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
260804     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.1ns 
260805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
263272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
264047     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
264076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.89ms 
264078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
264078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.5ns 
264079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266541     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
266542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
267320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
267379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.06ms 
267381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
267381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.1ns 
267382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269865     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
269865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
270642     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
270672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.7ms 
270674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
270675     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.5ns 
270676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
273159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
273935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
273955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.64ms 
273957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
273957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.4ns 
273958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
276427     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
277204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
277229     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.01ms 
277230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
277230     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97ns 
277231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
279723     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
280502     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
280523     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.12ms 
280524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
280524     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
280525     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
283001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
283778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
283807     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.12ms 
283809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
283809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.5ns 
283809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286272     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
286272     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
287049     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
287074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.91ms 
287076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
287076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
287077     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
289544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
290319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
290345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.54ms 
290348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
290348     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 256ns 
290350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292818     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
292818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
293594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
293619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.99ms 
293620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
293620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.1ns 
293621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
296101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
296876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
296897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.01ms 
296898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
296898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
296899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
299357     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
300131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
300161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.77ms 
300163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
300163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.4ns 
300164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302626     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
302626     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
303401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
303426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.92ms 
303428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
303428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96ns 
303428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
305917     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
306694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
306702     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.67ms 
306703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
306703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
306704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
309172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
309950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
309967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.67ms 
309968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
309968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
309969     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
312432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
313209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
313212     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
313214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
313214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
313214     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315691     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
315692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
316468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
316470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.01ns 
316473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
316473     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.4ns 
316474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318933     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
318933     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
319714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
319716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 751.51ns 
319723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
319723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.7ns 
319724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
322189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
322968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
322975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.77ms 
322977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
322977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.1ns 
322977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
325440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
326217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
326223     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
326224     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
326225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.8ns 
326225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
328692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
329472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
329484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.99ms 
329486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
329486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
329487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
331943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
332718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
332721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.01ms 
332723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
332723     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.7ns 
332723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
335180     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
335956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
335958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 670.01ns 
335960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
335960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
335960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
338415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
339192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
339198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
339200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
339200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
339200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
341657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
342435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
342438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 758.11ns 
342439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
342439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
342440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
344898     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
345674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
345677     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 588.31ns 
345678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
345678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
345679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
348137     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
348913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
348916     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 623.01ns 
348917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
348917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
348918     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
351377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
352152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
352156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
352157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
352157     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.3ns 
352158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
354613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
355390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
355399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.71ms 
355400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
355400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
355401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
357856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
358633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
358636     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
358638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
358638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78ns 
358639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
361095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
361877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
361884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.94ms 
361885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
361885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
361886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
364346     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
365122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
365126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.3ms 
365127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
365127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
365128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
367584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
368360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
368376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
368377     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
368377     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
368378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370845     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
370845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
371621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
371624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.77ms 
371625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
371625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
371626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374082     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
374083     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
374862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
374865     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
374866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
374866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
374867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
377325     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
378100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
378104     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.99ms 
378105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
378105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63ns 
378106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380565     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
380566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
381342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
381359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.31ms 
381360     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
381360     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
381361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
383823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
384598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
384603     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 722.81ns 
384606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
384606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.1ns 
384607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
387060     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
387836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
387873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.03ms 
387875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
387875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
387875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
390329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
391106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
391110     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
391111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
391111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.1ns 
391112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
393569     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
394344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
394366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.58ms 
394367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
394367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
394368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
396829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
397607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
397627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.55ms 
397628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
397628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
397629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
400097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
400874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
400897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.32ms 
400899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
400899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
400900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
403351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
404128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
404130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 622.91ns 
404131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
404131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
404132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
406591     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
407367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
407373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.8ms 
407374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
407374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
407375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
409830     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
410607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
410611     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
410612     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
410612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.5ns 
410613     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
413068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
413847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
413849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 852.61ns 
413850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
413850     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
413851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
416314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
417096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
417098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 924.51ns 
417099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
417100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
417100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
419560     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
420341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
420345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
420346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
420346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.9ns 
420347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422807     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
422807     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
423590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
423592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
423594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
423594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
423595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426061     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
426062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
426846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
426864     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.23ms 
426866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
426867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 208.1ns 
426867     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
429328     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
430111     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
430122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.58ms 
430124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
430124     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
430124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
432588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
433371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
433382     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.82ms 
433383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
433384     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
433384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
435840     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
436625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
436637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.56ms 
436638     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
436638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
436639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
439094     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
439878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
439882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.66ms 
439884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
439884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.2ns 
439884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
442344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
443127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
443133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
443134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
443134     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
443135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
445613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
446398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
446400     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 602.11ns 
446401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
446401     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
446402     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
448856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
449663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
449665     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
449667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
449667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.4ns 
449667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452101     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
452101     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
452909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
452911     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 765.41ns 
452912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
452912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
452913     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
455363     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
456171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
456181     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.34ms 
456182     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
456182     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
456183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
458635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
459443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
459447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.31ms 
459448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
459448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
459449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461887     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
461887     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
462696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
462703     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.72ms 
462704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
462704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
462705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465145     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
465145     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
465953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
465955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 761.71ns 
465957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
465957     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
465957     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
468389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
469196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
469198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 637.91ns 
469199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
469199     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
469200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
471637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
472446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
472450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
472451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
472451     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
472452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
474906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
475690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
475692     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
475693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
475694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.5ns 
475694     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
478151     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
478936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
478939     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
478941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
478941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
478941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
481397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
482204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
482207     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
482208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
482208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
482209     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
484647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
485455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
485460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.66ms 
485461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
485461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.5ns 
485462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
487894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
488704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
488708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.88ms 
488709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
488709     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.7ns 
488710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
491152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
491958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
491969     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ms 
491970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
491970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
491971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
494432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
495216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
495218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 624.31ns 
495219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
495219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.2ns 
495220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
497668     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
498453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
498459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5ms 
498461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
498461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
498461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
500911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
501717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
501719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 919.11ns 
501720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
501720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.9ns 
501721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
504154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
504154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
504963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
504965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.61ns 
504966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
504966     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
504967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
507402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
508208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
508215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.71ms 
508217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
508217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 202.1ns 
508218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
510678     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
511466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
511469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
511471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
511471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
511471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
513932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
514746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
514750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.86ms 
514751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
514751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
514752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
517187     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
517994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
517998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
517999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
517999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.2ns 
518000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
520428     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
521239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
521243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.21ms 
521245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
521245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.4ns 
521245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
523705     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
524492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
524506     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.14ms 
524508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
524508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.9ns 
524508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
526971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
527783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
527798     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.25ms 
527800     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
527800     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76ns 
527801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
530245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
531057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
531068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.49ms 
531069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
531069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
531070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
533505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
534314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
534324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.59ms 
534326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
534326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
534327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536779     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
536779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
537565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
537590     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.36ms 
537591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
537591     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
537592     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
540041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
540042     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
540850     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
540875     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.61ms 
540876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
540876     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.4ns 
540877     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
543306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
544118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
544141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.05ms 
544142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
544142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
544143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546600     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
546600     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
547385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
547399     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.98ms 
547400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
547400     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
547401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
549857     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
550664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
550695     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.95ms 
550696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
550696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
550697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
553128     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
553937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
553982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.43ms 
553984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
553984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
553985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
556441     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
557251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
557288     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.84ms 
557290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
557290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.7ns 
557290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
559730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
560541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
560585     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.2ms 
560586     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
560586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
560587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563040     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
563040     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
563827     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
563870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.47ms 
563871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
563871     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.9ns 
563872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
566323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
567136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
567250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 108.02ms 
567252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
567252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.3ns 
567253     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
569686     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
570498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
570505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.73ms 
570507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
570507     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.4ns 
570507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572955     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
572955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
573763     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
573770     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.74ms 
573771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
573772     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
573772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
576209     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
577018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
577024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.63ms 
577025     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
577025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.8ns 
577026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579478     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
579478     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
580285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
580303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.8ms 
580304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
580304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
580305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
582745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
583557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
583571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.57ms 
583572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
583572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
583573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586030     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
586030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
586816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
586820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
586821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
586821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.5ns 
586822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
589280     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
590087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
590103     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.47ms 
590105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
590105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
590106     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
592561     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
593350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
593366     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.53ms 
593367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
593368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
593368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
595817     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
596632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
596652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.87ms 
596653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
596653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
596654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
599113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
599113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
599898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
599901     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1ms 
599902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
599903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
599903     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
602350     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
602350     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
603159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
603162     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.84ms 
603163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
603163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
603164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605612     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
605612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
606398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
606405     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.03ms 
606406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
606406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
606407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608864     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
608864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
609674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
609680     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.17ms 
609681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
609681     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.8ns 
609682     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
612132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
612919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
613014     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 89.31ms 
613015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
613016     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.2ns 
613016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
615459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
616269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
616296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.85ms 
616298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
616298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 244.9ns 
616299     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
618758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
619566     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
619587     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.31ms 
619589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
619589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
619589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
622019     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
622019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
622826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
622828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 298.8ns 
622829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
622829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
622830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
625312     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
626119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
626313     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 183.08ms 
626315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
626316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.4ns 
626317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
628779     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
629594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
629644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.72ms 
629646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
629646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
629647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
632081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
632081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
632888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
632890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 345.9ns 
632891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
632891     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
632892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
635333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
636141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
636142     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 361.4ns 
636144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
636144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67ns 
636144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
638593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
639379     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
639381     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 367.2ns 
639382     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
639382     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.1ns 
639383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
641827     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
642633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
642635     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 500.91ns 
642636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
642637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
642637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
645079     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
645884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
645965     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
645979     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 92.05ms 
645981     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
645981     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.4ns 
645982     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
648447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
648447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
649234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
649280     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
649281     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.95ms 
649283     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
649283     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
649284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
651751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
652560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
652562     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ns 
652588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
652621     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
652638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
652642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
652648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
652650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
652651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
652653     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
652656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
652658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
652660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
652661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
652860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
652862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
652863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
652865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
652867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
653003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
653005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
653008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
653011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
653012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
653013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
653203     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
653206     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
653208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
653208     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
653210     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
653213     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
653379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
653382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
653383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
653384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
653385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
653386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
653394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
653395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
653396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
653398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
653400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
653401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
653410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
653412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
653412     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
653413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
653415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
653415     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
653560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
653561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
653563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
653674     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
653675     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)'' 
653678     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
653679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
653681     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
653682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
653683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
653685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
653690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
653691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
653693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
653693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
653694     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
653794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
653797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
653799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
653800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
653801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
653802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
653805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
653920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
653922     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
653923     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
653925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
653926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
653927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
653928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
653929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
654023     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
654025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
654146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
654150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
654156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
654157     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
654160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
654162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
654162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
654163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
654163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
654165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
654174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
654178     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
654276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
654277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
654279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
654281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
654281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
654282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
654284     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
654285     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
654333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
654338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
654444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
654446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
654447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
654449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
654450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
654450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
654567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
654571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
654574     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)'' 
654576     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
654577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
654580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
654581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
654582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
654591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
654597     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
654598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
654599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
654705     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
654707     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
654709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
654711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
654712     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
654713     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
654812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
654813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
654814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
654816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
654817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
654818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
654818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
654819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
654898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
654900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
654979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
654979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
654980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
654984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
654988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
654992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
655108     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
655110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
655110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
655111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
655121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
655199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
658638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
658639     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)'' 
658645     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
658646     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
658647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
658647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
658649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
658657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
658659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
658660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
658661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
658661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
658752     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
658756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
658757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
658758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
658759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
658759     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
658760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
658897     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
658898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
658899     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
658900     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
658901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
658901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
658902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
658903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
658978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
658979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
659058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
659062     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
659066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
659067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
659068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
659069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
659079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
659162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
659164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
659165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
659166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
659236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
659245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
659246     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)'' 
659248     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
659249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
659250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
659251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
659251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
659261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
659263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
659264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
659264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
659265     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
659350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
659352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
659353     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
659354     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
659355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
659444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
659449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
659450     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
659451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
659451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
659452     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
659453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
659549     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
659552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
659553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
659554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
659555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
659556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
659556     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
659557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
659558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
659559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
659560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
659561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
659562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
659562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
659563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
659648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
659650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
659656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
659731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
659810     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
659812     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
659813     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
659814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
659815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
659816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
659816     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
659817     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
659818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
659901     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
659907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
659996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
659997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
659998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
660000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
660000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
660001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
660001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
660002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
660007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
660008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
660086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
660092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
660097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
660195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
660196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
660197     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
660198     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
660199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
660199     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
660200     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
660201     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
660254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
660256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
660256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
660257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
660258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
660264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
660269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
660384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
660471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
660473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
660474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
660475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
660638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
660770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
660770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
663719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
663724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
663725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
663726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
663726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
663843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
663845     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
663846     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
663847     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
663849     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
663956     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
666882     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
669920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
669925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
669927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
669927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
669928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
670038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
670040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
670041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
670042     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)' ...' 
670043     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
671174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
671174     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
671175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673703     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
673703     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
674539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
674540     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
674541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
674546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
674557     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
674560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
674562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
674562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
674566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
674567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
674570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
674572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
674573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
674580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
674582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
674582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
674623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
674624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
674624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
674625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
674625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
674683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
674683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
674685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
674686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
674686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
674689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
674690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
674690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
674691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
674692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
674693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
674770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
674771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
674771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
674773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
674773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
674774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
674854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
674855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
674856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
674856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
674857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
674858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
674859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
674859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
674860     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
674861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
674861     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
674862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
674862     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
674863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
674863     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
674864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
674864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
674865     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
674866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
674869     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
674904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
674905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
674960     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
674961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
674962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
674964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
674964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
674965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
675012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
675014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
675016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
675017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
675019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
675019     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
675020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
675067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
675069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
675072     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
675120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
675171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
675172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 237.7ns 
675172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
677637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
678462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
678493     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.69ms