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

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

tests
0

failures
0

ignored
11m10.21s

duration
100%

successful

Tests

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

Standard output

322        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
348        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.16ms 
588        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609        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)

1580       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1584       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1588       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1588       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2784       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
8111       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.52s 
8185       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
8220       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.8ns 
8234       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
8235       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 742.41ns 
8241       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
11116      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
11118      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
12064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
12089      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.86ms 
12098      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
12098      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 185.8ns 
12100      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
14915      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
14915      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
15750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
15768      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.5ms 
15772      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
15772      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 172.3ns 
15776      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18559      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
18559      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
19433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
19440      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.56ms 
19443      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
19444      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 416.71ns 
19445      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22035      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.59s 
22036      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
22909      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
22922      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.91ms 
22927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
22928      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 717.8ns 
22929      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25537      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.61s 
25537      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
26375      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
26447      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 69.56ms 
26455      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
26456      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 978.01ns 
26458      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29018      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.56s 
29018      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
29858      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
29895      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.17ms 
29897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
29897      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.4ns 
29899      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32475      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.58s 
32475      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
33306      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
33310      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 693.91ns 
33311      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
33312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.7ns 
33313      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
35851      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
35851      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
36649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
36651      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 648.91ns 
36653      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
36654      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262ns 
36655      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
39182      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
39183      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
39974      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
39977      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 655.11ns 
39980      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
39980      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361ns 
39981      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
42480      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
42481      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
43275      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
43295      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.36ms 
43305      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
43305      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 454.31ns 
43307      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45851      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.54s 
45851      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
46669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
46673      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 702.31ns 
46677      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
46678      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 469.61ns 
46679      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49178      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
49178      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
49993      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
50023      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.55ms 
50025      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
50025      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 177ns 
50026      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52525      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
52525      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
53336      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
53364      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.15ms 
53366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
53366      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.1ns 
53368      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55837      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
55838      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
56652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
56763      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 102.5ms 
56767      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
56767      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 412.4ns 
56768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59244      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
59244      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
60073      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
60078      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.54ms 
60080      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
60080      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 252.1ns 
60082      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62570      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
62571      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
63357      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
63361      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.22ms 
63366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
63366      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.4ns 
63368      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
65847      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
65848      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
66633      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
66669      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.28ms 
66672      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
66672      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.11ns 
66673      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
69193      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
69194      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
69990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
70002      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.54ms 
70005      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
70006      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 371.5ns 
70007      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72505      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
72506      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
73319      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
73329      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.67ms 
73331      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
73331      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.5ns 
73332      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75797      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
75797      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
76605      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
76616      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.46ms 
76618      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
76618      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.1ns 
76619      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79115      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
79115      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
79923      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
79934      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.15ms 
79935      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
79935      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.5ns 
79936      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82406      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
82407      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
83306      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
83343      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.78ms 
83347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
83347      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.9ns 
83349      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85827      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
85827      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
86645      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
86649      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.33ms 
86652      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
86653      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 756.81ns 
86654      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
89113      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
89113      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
89920      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
89951      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.91ms 
89954      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
89954      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.3ns 
89955      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92464      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
92464      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
93245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
93287      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.21ms 
93289      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
93289      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.9ns 
93290      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95778      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
95778      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
96561      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
96591      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.32ms 
96593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
96593      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.3ns 
96594      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99081      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
99081      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
99888      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
99895      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
99896      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
99896      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.3ns 
99897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
102372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
103184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
103196     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.05ms 
103198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
103198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.1ns 
103199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105657     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
105657     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
106460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
106473     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.74ms 
106479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
106480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 478.31ns 
106481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108934     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
108935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
109737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
109745     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ms 
109747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
109748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 333.2ns 
109749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
112212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
113018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
113025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
113028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
113028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 375.9ns 
113029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115488     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
115488     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
116306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
116315     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
116318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
116318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 367.6ns 
116319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
118832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
118833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
119618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
119622     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
119624     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
119625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.4ns 
119626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
122159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.53s 
122159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
122941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
122955     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.7ms 
122958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
122958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 325.2ns 
122962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
125457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
125458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
126267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
126325     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.77ms 
126327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
126327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.4ns 
126333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
128778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
128778     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
129581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
129601     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.26ms 
129607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
129608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 386.1ns 
129609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
132107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
132107     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
132935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
132958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.08ms 
132960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
132961     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.8ns 
132962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135415     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
135415     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
136217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
136233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.89ms 
136235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
136235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121ns 
136236     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
138677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
139476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
139491     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.52ms 
139493     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
139493     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.5ns 
139494     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
141930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
141930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
142730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
142762     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.01ms 
142764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
142765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 347.2ns 
142767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
145241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
145242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
146016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
146019     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 958.31ns 
146021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
146021     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.7ns 
146022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
148500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
148500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
149275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
149282     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
149284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
149284     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.7ns 
149285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
151755     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
152554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
152561     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 
152563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
152563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.5ns 
152564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
155018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
155821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
155829     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.34ms 
155830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
155830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.5ns 
155831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
158288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
158289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
159104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
159121     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.13ms 
159122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
159123     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.7ns 
159123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
161587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
162388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
162396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.91ms 
162398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
162398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.2ns 
162398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
164868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
165677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
165681     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
165685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
165686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 516.11ns 
165687     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
168157     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
168961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
168965     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
168966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
168967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.3ns 
168967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
171444     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
172220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
172224     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.12ms 
172225     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
172225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
172226     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
174683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
174684     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
175459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
175516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.27ms 
175519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
175519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 307.5ns 
175520     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
178015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
178016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
178814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
178879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.96ms 
178881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
178881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 197.8ns 
178882     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
181331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
181331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
182131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
182135     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.47ms 
182137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
182137     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 315.7ns 
182139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
184613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
184614     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
185417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
185447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.96ms 
185448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
185449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.2ns 
185449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
187904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
188708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
188730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.57ms 
188732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
188732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.3ns 
188733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
191193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
191194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
191996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
191999     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
192000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
192000     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.5ns 
192001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194464     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
194464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
195263     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
195391     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 116.63ms 
195393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
195393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns 
195395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
197874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
197875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
198652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
198661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.84ms 
198662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
198662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.3ns 
198663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
201132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
201908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
201914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.43ms 
201916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
201916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.2ns 
201917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
204392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
205188     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
205202     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.76ms 
205204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
205204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.9ns 
205205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
207654     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
207654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
208455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
208466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.58ms 
208470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
208470     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 221.4ns 
208471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
210917     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
210918     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
211715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
211719     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.48ms 
211721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
211721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 184.9ns 
211722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
214169     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
214169     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
214972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
214976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.08ms 
214977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
214977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
214978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
217430     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
218233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
218248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.72ms 
218250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
218250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.4ns 
218251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
220692     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
221489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
221502     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.02ms 
221504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
221504     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.8ns 
221505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
223974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
223974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
224756     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
224767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.26ms 
224769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
224769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.3ns 
224770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
227252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
228035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
228038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
228041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
228041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.1ns 
228042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
230554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.51s 
230554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
231366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
231369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.31ms 
231370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
231370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.7ns 
231371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
233846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
234646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
234650     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.73ms 
234652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
234652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.2ns 
234652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
237086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
237885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
237888     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 912.91ns 
237889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
237889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.2ns 
237890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
240329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
240329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
241129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
241131     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 527.61ns 
241132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
241133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
241133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
243566     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
243566     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
244401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
244406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
244409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
244409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.3ns 
244410     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
246861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
247662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
247664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 752.71ns 
247666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
247667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 219.1ns 
247668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
250140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
250921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
250975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.87ms 
250977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
250977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251ns 
250978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
253480     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
254260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
254284     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.83ms 
254286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
254286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.7ns 
254287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
256756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
256756     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
257563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
257586     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.02ms 
257589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
257589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.9ns 
257590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
260043     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
260842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
260872     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.78ms 
260873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
260873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.1ns 
260874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
263330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
263330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
264133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
264152     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.77ms 
264153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
264153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
264154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
266590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
266590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
267390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
267425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.08ms 
267427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
267427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.7ns 
267428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
269873     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
270671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
270690     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.28ms 
270692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
270692     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115ns 
270693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
273143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
273944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
273958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.25ms 
273960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
273960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.1ns 
273961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276429     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
276429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
277210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
277227     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.98ms 
277228     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
277228     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
277229     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279704     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
279704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
280484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
280498     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.84ms 
280499     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
280499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.9ns 
280500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
282993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
283793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
283810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.86ms 
283812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
283812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.5ns 
283813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
286253     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
287051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
287067     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.79ms 
287069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
287069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.8ns 
287069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
289521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
289521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
290324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
290341     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.31ms 
290342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
290342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.3ns 
290343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
292771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
292771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
293567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
293582     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.35ms 
293584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
293584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
293585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
296015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
296016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
296820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
296834     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.48ms 
296836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
296836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
296837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
299287     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
299287     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
300087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
300102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.21ms 
300104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
300104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.4ns 
300105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
302544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
303314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
303330     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.13ms 
303332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
303332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 
303332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
305793     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
305793     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
306565     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
306571     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
306572     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
306573     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
306573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
309041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
309845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
309856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.79ms 
309858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
309858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.4ns 
309859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
312336     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
313139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
313143     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.85ms 
313144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
313144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
313145     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
315586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
316383     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
316386     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 574.41ns 
316388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
316388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.6ns 
316389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
318826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
319627     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
319630     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 688.11ns 
319631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
319631     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
319632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
322067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
322871     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
322876     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
322878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
322878     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.6ns 
322878     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
325331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
325331     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
326133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
326138     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.16ms 
326141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
326141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.5ns 
326142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
328608     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
329385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
329395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.35ms 
329396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
329397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.2ns 
329397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
331863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
332635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
332638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.67ms 
332639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
332640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.4ns 
332640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
335116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
335922     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
335925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 479.6ns 
335927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
335927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.5ns 
335928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338379     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
338380     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
339183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
339189     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.38ms 
339192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
339192     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.8ns 
339193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
341628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
342423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
342426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 659.71ns 
342427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
342427     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
342428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
344867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
344867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
345666     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
345668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 577.9ns 
345670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
345670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
345671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
348094     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
348095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
348893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
348896     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 528.8ns 
348898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
348898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.4ns 
348899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
351339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
351339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
352143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
352146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
352148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
352148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.6ns 
352149     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 
355385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
355392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.92ms 
355393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
355393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.1ns 
355394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357852     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
357852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
358625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
358628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.68ms 
358629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
358630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.1ns 
358630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
361078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
361849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
361855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
361856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
361856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72ns 
361857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
364316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
364317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
365114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
365120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
365128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
365128     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 262.4ns 
365129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367564     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
367564     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
368363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
368378     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.03ms 
368380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
368380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
368381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370829     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
370829     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
371629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
371634     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
371635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
371635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.7ns 
371636     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374089     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
374090     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
374894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
374897     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 994.81ns 
374898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
374898     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
374899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
377351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
377351     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
378155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
378159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
378160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
378161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.2ns 
378161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
380607     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
380607     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
381412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
381425     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.11ms 
381426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
381426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.9ns 
381427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
383884     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
384656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
384661     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 338.4ns 
384663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
384663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
384664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
387103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
387876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
387902     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.7ms 
387904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
387904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
387904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390358     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
390358     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
391158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
391161     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.6ms 
391163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
391163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
391164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
393595     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
393595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
394389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
394404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.01ms 
394405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
394405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88ns 
394406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396827     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
396828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
397623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
397638     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.49ms 
397640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
397640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.8ns 
397641     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
400074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
400869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
400887     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.87ms 
400889     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
400889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
400890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403319     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
403319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
404119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
404122     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 583.5ns 
404124     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
404125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.1ns 
404126     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
406553     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
407348     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
407353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.41ms 
407354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
407354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.4ns 
407355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
409811     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
410588     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
410592     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
410593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
410593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
410594     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
413062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
413062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
413843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
413845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 840.51ns 
413847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
413847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.3ns 
413847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416307     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
416308     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
417112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
417114     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 820.51ns 
417116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
417116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61ns 
417116     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
419572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
420373     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
420376     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
420378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
420378     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
420378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
422800     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
423602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
423605     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.2ms 
423606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
423606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
423607     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
426037     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
426842     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
426849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.05ms 
426851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
426851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.9ns 
426851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429306     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
429306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
430081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
430088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
430089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
430090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
430090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
432544     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
433365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
433371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.57ms 
433374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
433374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
433374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
435845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
436660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
436668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.7ms 
436670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
436670     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.4ns 
436671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
439133     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
439942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
439946     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2ms 
439947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
439947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
439948     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
442383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
443193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
443197     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
443198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
443198     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
443199     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
445655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
445655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
446441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
446443     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 960.11ns 
446445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
446445     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
446446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
448902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
448902     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
449708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
449711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 974.91ns 
449712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
449712     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
449713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
452131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
452131     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
452935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
452937     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 892.51ns 
452939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
452939     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
452939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
455361     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
455361     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
456170     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
456180     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.46ms 
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 78.5ns 
456183     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458636     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
458636     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
459420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
459423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
459424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
459424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
459425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
461874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
461874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
462681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
462687     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
462689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
462689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 207.7ns 
462690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465117     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
465117     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
465923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
465926     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 825.21ns 
465927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
465927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
465928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
468374     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
469155     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
469157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 612.3ns 
469159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
469159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.1ns 
469159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471613     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
471613     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
472421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
472424     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
472425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
472426     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
472426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
474863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
475670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
475672     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 759.71ns 
475674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
475674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
475675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
478122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
478904     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
478906     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 990.81ns 
478908     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
478908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
478909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
481354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
481354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
482161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
482164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
482165     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
482165     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
482166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
484595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
485398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
485402     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.1ms 
485404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
485404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.5ns 
485404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487848     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
487848     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
488630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
488632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 886.61ns 
488634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
488634     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
488634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
491078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
491884     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
491893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.84ms 
491895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
491895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
491895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
494334     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
495139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
495141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 614.11ns 
495143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
495143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
495143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
497584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
498397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
498404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.48ms 
498407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
498407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.1ns 
498408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
500859     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
500859     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
501671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
501674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
501677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
501677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.6ns 
501677     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.48s 
504154     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
504940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
504944     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 787.41ns 
504946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
504946     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
504946     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
507406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
508215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
508219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
508220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
508221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.6ns 
508221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
510655     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
510655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
511459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
511462     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 836.41ns 
511463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
511463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.9ns 
511464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513911     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
513912     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
514717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
514720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
514721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
514721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
514722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
517149     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
517955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
517958     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
517959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
517959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 188.2ns 
517960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
520407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
521213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
521217     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.05ms 
521218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
521218     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
521219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523652     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
523652     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
524459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
524466     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.27ms 
524468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
524468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.2ns 
524468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
526912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
526913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
527718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
527726     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.75ms 
527729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
527729     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 211.8ns 
527730     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
530154     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
530155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
530956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
530962     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.16ms 
530964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
530964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70ns 
530964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
533407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
533407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
534210     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
534216     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.29ms 
534217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
534217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
534218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
536640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
536640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
537445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
537456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.86ms 
537458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
537458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.7ns 
537458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539904     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
539904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
540708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
540718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ms 
540720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
540720     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.2ns 
540721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
543147     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
543951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
543960     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.21ms 
543962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
543962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.3ns 
543963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546406     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
546406     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
547212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
547219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.84ms 
547220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
547220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
547221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.42s 
549645     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
550448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
550468     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.25ms 
550469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
550469     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
550470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
552964     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.49s 
552965     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
553772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
553794     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.07ms 
553796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
553796     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.7ns 
553797     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
556251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
556252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
557037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
557056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.62ms 
557057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
557057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.3ns 
557058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559519     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
559520     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
560324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
560342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.64ms 
560343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
560343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
560344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
562797     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
562798     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
563601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
563619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.12ms 
563620     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
563620     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
563621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
566048     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
566048     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
566854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
566899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.48ms 
566901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
566901     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.5ns 
566902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
569356     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
569356     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
570167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
570171     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.58ms 
570173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
570173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.9ns 
570173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572635     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
572635     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
573450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
573455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.99ms 
573456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
573456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.7ns 
573457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
575894     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
576704     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
576708     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.92ms 
576710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
576710     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.4ns 
576710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579186     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
579186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
580012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
580024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.63ms 
580026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
580026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
580026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
582492     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
582493     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
583301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
583307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.14ms 
583309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
583309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
583309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
585750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
585751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
586557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
586560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
586561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
586561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
586562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
589007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
589007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
589810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
589820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.48ms 
589821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
589821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
589822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
592258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
593062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
593072     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.01ms 
593074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
593074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.21ns 
593074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
595512     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
595512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
596293     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
596306     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.95ms 
596309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
596309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 201.01ns 
596310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598748     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
598748     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
599553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
599555     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 990.13ns 
599557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
599557     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.3ns 
599558     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601996     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
601996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
602804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
602808     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
602809     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
602809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.3ns 
602810     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.43s 
605245     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
606050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
606056     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.03ms 
606058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
606058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 137.4ns 
606059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
608502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
609285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
609289     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.6ms 
609291     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
609291     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.8ns 
609292     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
611731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
611732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
612536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
612577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.72ms 
612579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
612579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
612580     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
615064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
615064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
615873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
615893     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.5ms 
615895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
615895     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.5ns 
615895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
618343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
618343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
619147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
619158     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.47ms 
619159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
619159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
619160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
621599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
622419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
622422     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 176.4ns 
622424     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
622424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 204ns 
622425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624884     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
624885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
625690     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
625767     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 66.8ms 
625769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
625769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
625770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
628226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.46s 
628227     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
629016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
629050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.64ms 
629052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
629052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79ns 
629053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
631495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
632300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
632302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 188.61ns 
632304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
632304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
632304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
634744     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
635549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
635551     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 218.91ns 
635552     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
635552     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
635553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.44s 
637995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
638801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
638803     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 230.21ns 
638805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
638805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
638806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.45s 
641260     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
642068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
642070     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 385.01ns 
642071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
642071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.2ns 
642072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
644537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.47s 
644538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
645352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
645440     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
645452     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 98.3ms 
645456     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
645456     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.51ns 
645457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
647960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.5s 
647960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
648772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
648820     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
648821     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.36ms 
648823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
648823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
648824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
651303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.48s 
651303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
652113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
652115     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.2ns 
652149     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
652204     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
652222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
652229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
652246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
652247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
652250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
652251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
652257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
652261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 17, source line: 59, command: 'instantiate var=iv with='v_x_0' occ=1' 
652264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
652269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
652523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
652524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
652527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 64, command: 'instantiate var=iv with='v_y_0' occ=1' 
652528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
652530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
652663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
652664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
652668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
652669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 190, source line: 72, command: 'instantiate var=iv with='v_x_0' occ=2' 
652670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
652673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
652851     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
652853     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
652855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
652856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 78, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
652857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
652859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
652992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
652994     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
652995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
652996     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 85, command: 'instantiate var=iv with='jv_0' occ=1' 
652997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
652998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
653007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
653008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
653011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 435, source line: 91, command: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
653011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 92, command: 'instantiate hide var=iv with='jv_1' occ=1' 
653013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
653015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
653024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
653026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
653027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 449, source line: 98, command: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
653028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
653029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
653030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
653151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
653153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
653154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
653261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
653263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 109, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
653264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
653267     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
653268     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
653269     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
653271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
653272     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
653275     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
653276     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 687, source line: 120, command: 'instantiate hide var='iv' with='v_x_0' occ=1' 
653278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
653279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
653280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
653374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
653378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
653379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
653380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
653381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
653382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
653383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
653491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
653492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
653493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
653495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
653496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
653496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
653497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
653498     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
653589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
653591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
653675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
653679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
653684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
653685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
653686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
653687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
653688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
653688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
653689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
653690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
653697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
653702     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
653796     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
653797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
653798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
653799     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
653800     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
653801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
653801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
653802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
653848     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
653854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
653945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 166, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
653946     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
653947     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [105] goal: 1399, source line: 170, command: 'instantiate hide var=iv with='v_x_0'' 
653949     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [106] goal: 1400, source line: 171, command: 'instantiate hide var=jv with='v_y_0'' 
653951     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
653952     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
654090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
654094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 175, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
654095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 177, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
654097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
654098     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
654099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
654100     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
654101     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
654111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
654112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [118] goal: 1558, source line: 187, command: 'instantiate hide var=iv with='v_y_0'' 
654114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
654115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
654220     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
654221     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
654223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
654224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
654224     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
654225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
654340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
654341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
654343     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
654344     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
654345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
654345     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
654346     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
654347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
654476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
654477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
654553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
654554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
654555     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
654559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
654563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
654568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
654689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
654690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
654691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
654692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
654703     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
654790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
658439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 221, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
658440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 224, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
658444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
658446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
658447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
658448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
658448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
658457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
658458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [157] goal: 4287, source line: 234, command: 'instantiate hide var=iv with='v_x_0'' 
658459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
658460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
658461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
658554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
658558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
658559     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
658560     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
658561     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
658562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
658563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
658658     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
658659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
658660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
658661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
658662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
658663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
658663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
658664     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
658740     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
658741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
658815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
658820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
658824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
658825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
658827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
658828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
658838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
658964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
658965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
658966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
658967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
659038     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
659048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 270, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
659049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 273, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
659050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
659052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
659052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
659053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
659054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
659066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
659067     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
659068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [199] goal: 4978, source line: 284, command: 'instantiate hide var=jv with='v_x_0'' 
659069     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
659070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
659160     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [202] goal: 4981, source line: 287, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
659161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
659162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [204] goal: 5094, source line: 289, command: 'instantiate hide var=jv with='v_y_0'' 
659163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
659164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
659255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
659259     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
659260     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
659261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
659262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
659262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
659263     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
659362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
659364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
659365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
659366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
659367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
659368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
659368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
659369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
659370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
659371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
659372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
659372     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
659373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
659374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
659374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
659461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
659463     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
659469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
659544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
659622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
659623     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
659624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
659625     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
659626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
659626     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
659627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
659627     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
659628     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
659711     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
659717     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
659805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
659806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
659806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
659807     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
659808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
659808     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
659809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
659809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
659814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
659815     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
659893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
659898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
659908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
660005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
660006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
660007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
660008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
660008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
660008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
660009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
660009     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
660063     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
660064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
660065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
660065     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
660066     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
660071     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
660076     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
660192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
660280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
660281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
660281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
660282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
660448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
660536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 371, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
660536     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
663546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
663551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
663552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [282] goal: 8784, source line: 381, command: 'instantiate hide var=jv with='v_y_0'' 
663553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
663554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
663667     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [285] goal: 8787, source line: 384, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
663668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
663669     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [287] goal: 8910, source line: 386, command: 'instantiate hide var=jv with='v_x_0'' 
663670     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
663671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
663773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
666654     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
669762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
669766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [293] goal: 12633, source line: 399, command: 'instantiate hide var=iv with='v_x_0'' 
669767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
669768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
669769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
669883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [297] goal: 12637, source line: 403, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
669883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [298] goal: 12757, source line: 404, command: 'instantiate hide var=iv with='v_y_0'' 
669884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
669885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [300] goal: 12759, source line: 406, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
669886     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
670975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
670975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.1ns 
670976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.57s 
673542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
674369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
674371     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
674371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
674380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 10, source line: 51, command: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
674390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
674393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
674395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
674396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
674402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
674402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
674407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
674408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
674410     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
674421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
674421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
674422     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
674474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
674475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
674476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
674476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
674476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
674544     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
674545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
674545     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
674546     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
674547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
674551     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
674552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
674552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
674553     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
674554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
674554     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
674634     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
674635     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
674636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
674637     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
674638     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
674639     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
674720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
674721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
674722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
674722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
674723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
674724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
674724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
674725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
674726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
674726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
674727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
674727     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
674728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
674728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
674729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
674729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
674730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
674730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
674731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
674734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
674766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
674768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
674820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
674822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
674823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
674824     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
674825     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
674826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
674876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
674879     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
674880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
674881     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
674883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
674884     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
674885     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
674936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
674939     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
674942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
675005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
675071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
675072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 981.22ns 
675073     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677589     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.52s 
677589     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
678447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
678463     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.67ms