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

198

tests

0

failures

0

ignored

12m40.69s

duration

100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.651s passed
powPositiveConcrete data()[101] 3.712s passed
powGeq1Concrete data()[102] 3.704s passed
pow2InIntLower data()[103] 3.675s passed
pow2InIntUpper data()[104] 3.689s passed
logSelfConcrete data()[105] 3.715s passed
log1Concrete data()[106] 3.680s passed
logProduct data()[107] 3.654s passed
logTimesBaseConcrete data()[108] 3.674s passed
logProdIdentity data()[109] 3.733s passed
moduloByteIsInByte data()[10] 3.716s passed
logProdIdentityConcrete data()[110] 3.687s passed
logPowIdentity data()[111] 3.674s passed
logPowIdentityConcrete data()[112] 3.740s passed
logPositive data()[113] 3.677s passed
logPositiveConcrete data()[114] 3.688s passed
logMono data()[115] 3.682s passed
logMonoConcrete data()[116] 3.648s passed
powLogLess data()[117] 3.686s passed
powLogMore2 data()[118] 3.688s passed
logLessThanPow data()[119] 3.717s passed
moduloCharIsInChar data()[11] 3.720s passed
logLessThanPowConcrete data()[120] 3.651s passed
logSqueeze data()[121] 3.694s passed
ifthenelse_equals data()[122] 3.671s passed
ifthenelse_equals_1 data()[123] 3.697s passed
ifthenelse_equals_2 data()[124] 3.664s passed
disjointWithSingleton1 data()[125] 3.670s passed
disjointWithSingleton2 data()[126] 3.735s passed
disjointArrayRanges data()[127] 3.693s passed
disjointArrayRangeAllFields1 data()[128] 3.778s passed
disjointArrayRangeAllFields2 data()[129] 3.736s passed
div_unique1 data()[12] 3.895s passed
seqSelfDefinition data()[130] 3.744s passed
seqOutsideValue data()[131] 3.720s passed
castedGetAny data()[132] 3.746s passed
seqGetAlphaCast data()[133] 3.703s passed
getOfSeqSingleton data()[134] 3.692s passed
getOfSeqSingletonConcrete data()[135] 3.684s passed
getOfSeqConcat data()[136] 3.687s passed
getOfSeqSub data()[137] 3.647s passed
getOfSeqReverse data()[138] 3.760s passed
lenOfSeqEmpty data()[139] 3.719s passed
div_unique2 data()[13] 3.830s passed
lenOfSeqSingleton data()[140] 3.679s passed
lenOfSeqConcat data()[141] 3.726s passed
lenOfSeqSub data()[142] 3.665s passed
lenOfSeqReverse data()[143] 3.741s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.747s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.688s passed
getOfSeqSingletonEQ data()[146] 3.744s passed
getOfSeqConcatEQ data()[147] 3.715s passed
getOfSeqSubEQ data()[148] 3.684s passed
getOfSeqReverseEQ data()[149] 3.725s passed
div_exists data()[14] 3.938s passed
lenOfSeqEmptyEQ data()[150] 3.699s passed
lenOfSeqSingletonEQ data()[151] 3.699s passed
lenOfSeqConcatEQ data()[152] 3.711s passed
lenOfSeqSubEQ data()[153] 3.711s passed
lenOfSeqReverseEQ data()[154] 3.723s passed
getOfSeqDefEQ data()[155] 3.712s passed
lenOfSeqDefEQ data()[156] 3.705s passed
seqConcatWithSeqEmpty1 data()[157] 3.701s passed
seqConcatWithSeqEmpty2 data()[158] 3.697s passed
seqReverseOfSeqEmpty data()[159] 3.670s passed
div_one data()[15] 3.799s passed
subSeqComplete data()[160] 3.697s passed
subSeqTailR data()[161] 3.758s passed
subSeqTailL data()[162] 3.723s passed
subSeqTailEQR data()[163] 3.723s passed
subSeqTailEQL data()[164] 3.711s passed
seqDef_split data()[165] 3.742s passed
seqDef_induction_upper data()[166] 3.732s passed
seqDef_induction_upper_concrete data()[167] 3.714s passed
seqDef_induction_lower data()[168] 3.698s passed
seqDef_induction_lower_concrete data()[169] 3.720s passed
jdiv_one data()[16] 3.805s passed
seqDef_split_in_three data()[170] 3.749s passed
seqDef_empty data()[171] 3.669s passed
seqDef_one_summand data()[172] 3.676s passed
seqDef_lower_equals_upper data()[173] 3.702s passed
seqDefOfSeq data()[174] 3.670s passed
seqSelfDefinitionEQ2 data()[175] 3.645s passed
indexOfSeqSingleton data()[176] 3.696s passed
indexOfSeqConcatFirst data()[177] 3.714s passed
indexOfSeqConcatSecond data()[178] 3.698s passed
indexOfSeqSub data()[179] 3.626s passed
div_zero data()[17] 3.861s passed
lenOfArray2seq data()[180] 3.724s passed
getAnyOfArray2seq data()[181] 3.700s passed
getOfArray2seq data()[182] 3.667s passed
getAnyOfNPermInv data()[183] 3.678s passed
seqNPermRange data()[184] 3.739s passed
seqPermTrans data()[185] 3.727s passed
seqPermRefl data()[186] 3.746s passed
seqPermSplit data()[187] 3.730s passed
seqNPermRight data()[188] 3.849s passed
seqPermFromSwap data()[189] 3.770s passed
divResZero1 data()[18] 3.719s passed
seqPermTransAlt0 data()[190] 3.704s passed
seqPermTransAlt1 data()[191] 3.695s passed
seqPermTransAlt2 data()[192] 3.671s passed
seqPermTransAlt3 data()[193] 3.711s passed
seqPermForall data()[194] 3.788s passed
seqPermExists data()[195] 3.744s passed
schiffl_lemma_2 data()[196] 25.443s passed
schiffl_thm_1 data()[197] 4.588s passed
eqSameSeq data()[198] 4.054s passed
divResZero2 data()[19] 3.711s passed
eqTermCut data()[1] 4.420s passed
divResOne1 data()[20] 3.783s passed
divResOne2 data()[21] 3.722s passed
div_cancel1 data()[22] 3.706s passed
div_cancel2 data()[23] 3.703s passed
divAddMultDenom data()[24] 3.759s passed
divMinus data()[25] 3.786s passed
divMinusDenom data()[26] 3.762s passed
divLeastDPos data()[27] 3.753s passed
divLeastDNeg data()[28] 3.739s passed
divGreatestDPos data()[29] 3.767s passed
equivAllRight data()[2] 4.205s passed
divGreatestDNeg data()[30] 3.761s passed
divIncreasingPos data()[31] 3.817s passed
divIncreasingNeg data()[32] 3.697s passed
jdiv_zero data()[33] 3.687s passed
jdivPulloutMinusNum data()[34] 3.675s passed
jdivPulloutMinusDenom data()[35] 3.775s passed
jdiv_uniquePosPos data()[36] 3.689s passed
jdiv_uniquePosNeg data()[37] 3.717s passed
jdiv_uniqueNegPos data()[38] 3.669s passed
jdiv_uniqueNegNeg data()[39] 3.706s passed
irrflConcrete1 data()[3] 4.015s passed
jdivMultDenom1 data()[40] 3.706s passed
jdivMultDenom2 data()[41] 3.663s passed
mod_geZero data()[42] 3.739s passed
mod_lessDenom data()[43] 3.725s passed
jmod_NumPos data()[44] 3.748s passed
jmod_NumNeg data()[45] 3.701s passed
jmod_geZero data()[46] 3.758s passed
jmodNumZero data()[47] 3.753s passed
jmod_pulloutminusNum data()[48] 3.730s passed
jmod_pulloutminusDenom data()[49] 3.686s passed
irrflConcrete2 data()[4] 3.910s passed
jmodUnique1 data()[50] 3.813s passed
jmodUnique2 data()[51] 3.789s passed
intDivRem data()[52] 3.700s passed
jmodjmod data()[53] 3.811s passed
jmodDivisible data()[54] 3.726s passed
jmodDivisibleRep data()[55] 3.700s passed
jdivAddMultDenom data()[56] 3.768s passed
jmodAltZero data()[57] 3.688s passed
jmodAddMultDenomZero data()[58] 3.719s passed
polyDiv_zero data()[59] 3.670s passed
cancel_gtPos data()[5] 3.937s passed
polyMod_ltdivDenom data()[60] 3.707s passed
bsum_empty data()[61] 3.637s passed
bsum_induction_upper data()[62] 3.629s passed
bsum_induction_lower data()[63] 3.740s passed
bsum_num_of_bounds data()[64] 3.727s passed
bsum_num_of_bounds2 data()[65] 3.722s passed
bsum_induction_upper2 data()[66] 3.652s passed
bsum_induction_upper_concrete data()[67] 3.667s passed
bsum_induction_upper_concrete_2 data()[68] 3.704s passed
bsum_induction_upper2_concrete data()[69] 3.678s passed
cancel_gtNeg data()[6] 3.842s passed
bsum_induction_lower_concrete data()[70] 3.706s passed
bsum_induction_lower2 data()[71] 3.667s passed
bsum_induction_lower2_concrete data()[72] 3.769s passed
bsum_positive data()[73] 3.759s passed
bsum_upper_bound data()[74] 3.770s passed
bsum_lower_bound data()[75] 3.785s passed
bsum_positive_lower_bound_element data()[76] 3.699s passed
bsum_sub_same_index data()[77] 3.695s passed
bsum_less_same_index data()[78] 3.715s passed
bsum_equal_except_one_index data()[79] 3.722s passed
moduloIntIsInInt data()[7] 3.879s passed
bsum_num_of_is_max data()[80] 3.682s passed
bsum_num_of_is_max2 data()[81] 3.699s passed
bsum_num_of_is_max3 data()[82] 3.638s passed
bsum_num_of_is_max4 data()[83] 3.727s passed
bsum_num_of_lt_max data()[84] 3.738s passed
bsum_num_of_lt_max2 data()[85] 3.678s passed
bsum_num_of_lt_max3 data()[86] 3.729s passed
bsum_num_of_lt_max4 data()[87] 3.661s passed
bsum_num_of_gt0 data()[88] 3.696s passed
bsum_num_of_gt0_alt data()[89] 3.672s passed
moduloLongIsInLong data()[8] 3.756s passed
bsum_add_concrete data()[90] 3.676s passed
bprod_all_positive data()[91] 3.674s passed
bprod_split data()[92] 3.680s passed
powConcrete0 data()[93] 3.646s passed
powConcrete1 data()[94] 3.693s passed
powSplitFactor data()[95] 3.689s passed
powAdd data()[96] 3.733s passed
powMono data()[97] 3.705s passed
powMonoConcrete data()[98] 3.675s passed
powMonoConcreteRight data()[99] 3.629s passed
moduloShortIsInShort data()[9] 3.793s passed

Standard output

618        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
643        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 8.1ms 
873        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
894        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)

1791       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1794       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1797       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
1797       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
3407       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
9663       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.79s 
9731       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
9769       DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39ns 
9783       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
9785       DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.95ms 
9790       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13043      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
13046      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14168      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14195      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.02ms 
14205      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14205      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.21ns 
14208      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
17312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
17313      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
18393      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
18407      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10ms 
18411      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
18411      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 644.24ns 
18413      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
21427      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
21428      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
22417      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
22424      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
22427      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
22428      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 794.24ns 
22429      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25375      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
25376      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
26330      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
26335      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.64ms 
26337      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
26337      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.01ns 
26338      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29222      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
29222      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
30186      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
30271      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 76.44ms 
30274      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
30276      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.24ms 
30277      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33136      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
33137      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
34088      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
34113      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.47ms 
34118      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
34118      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 165.31ns 
34119      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37045      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
37045      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
37991      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
37994      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 759.44ns 
37996      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
37996      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 125.01ns 
37997      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
40840      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
40841      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
41748      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
41750      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 673.04ns 
41752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
41752      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.41ns 
41753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
44602      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
44602      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
45540      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
45543      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 615.53ns 
45545      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
45546      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.02ns 
45547      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
48312      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
48312      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
49256      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
49259      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 617.83ns 
49262      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
49262      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 378.62ns 
49263      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52029      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
52030      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
52973      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
52979      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.06ms 
52983      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
52983      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 421.12ns 
52984      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
55910      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
55910      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
56824      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
56875      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.35ms 
56876      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
56876      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.11ns 
56877      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
59677      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
59677      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
60647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
60700      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.1ms 
60709      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
60709      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 281.42ns 
60712      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
63533      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
63533      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
64464      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
64643      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 171.1ms 
64647      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
64648      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 419.22ns 
64649      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
67504      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
67505      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
68438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
68444      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.15ms 
68446      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
68446      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.02ns 
68448      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
71291      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
71293      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
72245      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
72249      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
72253      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
72253      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 381.92ns 
72254      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75074      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
75075      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
76043      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
76111      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.77ms 
76114      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
76114      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149.41ns 
76115      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78882      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
78882      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
79817      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
79831      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.96ms 
79834      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
79835      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 985.75ns 
79836      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
82618      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
82618      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
83529      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
83541      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.5ms 
83544      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
83545      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.22ns 
83551      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
86372      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
86373      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
87304      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
87323      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.03ms 
87327      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
87327      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 148.41ns 
87328      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90068      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
90068      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
91018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
91046      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.82ms 
91052      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
91054      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.86ms 
91055      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
93822      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
93823      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
94737      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
94757      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.87ms 
94758      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
94758      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.31ns 
94759      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97558      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
97558      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
98448      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
98459      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
98461      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
98461      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 128.81ns 
98462      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
101258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
102181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
102218     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.56ms 
102220     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
102220     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.81ns 
102221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
104998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
104998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
105953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
106003     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.91ms 
106006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
106007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 379.42ns 
106008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
108794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
108794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
109732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
109766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.5ms 
109767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
109768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.41ns 
109769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
112572     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
112572     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
113511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
113519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.2ms 
113522     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
113522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.22ns 
113523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116290     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
116291     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
117237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
117257     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.98ms 
117261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
117261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 630.53ns 
117262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120072     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
120074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
121013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
121026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.6ms 
121027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
121028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 222.71ns 
121029     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
123874     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
124780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
124787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.02ms 
124788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
124788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.11ns 
124789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127640     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
127640     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
128596     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
128604     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.76ms 
128605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
128605     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.31ns 
128606     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
131373     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
132295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
132302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.79ms 
132303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
132303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.31ns 
132304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
135064     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
135985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
135989     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
135990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
135990     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 107.91ns 
135991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138769     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
138769     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
139653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
139663     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.16ms 
139664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
139664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.11ns 
139665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
142472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
143403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
143438     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.99ms 
143440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
143440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.01ns 
143441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
146195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
147103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
147126     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.75ms 
147129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
147129     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.81ns 
147131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
149888     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
149888     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
150830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
150845     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.95ms 
150846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
150846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.41ns 
150847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153596     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
153597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
154491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
154512     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.81ms 
154515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
154515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 357.72ns 
154516     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157286     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
157286     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
158204     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
158219     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.97ms 
158221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
158222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 343.02ns 
158223     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
160970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
160970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
161893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
161925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.52ms 
161927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
161927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 305.82ns 
161928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164686     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
164687     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
165585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
165588     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 954.65ns 
165590     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
165590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 187.91ns 
165591     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168391     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
168391     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
169323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
169327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
169328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
169328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
169329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
172119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
173044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
173052     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.43ms 
173053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
173053     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.5ns 
173054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175863     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
175863     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
176793     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
176801     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.43ms 
176802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
176802     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.61ns 
176803     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179586     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
179586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
180484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
180501     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.55ms 
180503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
180503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.21ns 
180504     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
183323     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
184251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
184259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
184261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
184261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.5ns 
184262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187071     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
187072     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
188009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
188012     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
188015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
188015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 345.82ns 
188019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
190773     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
191739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
191742     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.58ms 
191744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
191744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.2ns 
191745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194534     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
194534     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
195425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
195429     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
195430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
195430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.11ns 
195431     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
198225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
199181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
199240     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.23ms 
199243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
199244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 327.92ns 
199245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
202024     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
202024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
202959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
203029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 61.4ms 
203032     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
203033     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 200.61ns 
203033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
205823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
206726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
206730     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
206731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
206731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 171.41ns 
206732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209546     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
209546     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
210498     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
210541     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39ms 
210543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
210543     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.72ns 
210544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
213314     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
213314     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
214246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
214267     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.29ms 
214269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
214269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102.61ns 
214270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217032     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
217032     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
217964     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
217967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 958.35ns 
217968     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
217968     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.4ns 
217970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
220741     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
221630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
221735     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 93.44ms 
221737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
221737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns 
221738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224505     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
224505     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
225415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
225423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.49ms 
225425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
225425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.7ns 
225426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
228210     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
228210     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
229135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
229141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.83ms 
229144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
229144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 270.12ns 
229148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
231889     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
232796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
232812     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.96ms 
232814     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
232815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 294.42ns 
232816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235588     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
235588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
236474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
236518     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.75ms 
236521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
236521     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.1ns 
236521     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
239253     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
239254     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
240153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
240157     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
240158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
240158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
240159     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242862     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
242862     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
243781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
243785     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
243787     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
243787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.9ns 
243788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
246622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
247511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
247525     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.63ms 
247528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
247528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 306.02ns 
247529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
250318     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
250319     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
251241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
251253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.11ms 
251254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
251254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 98.11ns 
251255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
254022     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
254022     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
254962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
254974     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.15ms 
254976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
254977     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 279.22ns 
254979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
257696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
258622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
258626     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 945.25ns 
258628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
258628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 251.41ns 
258629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261402     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
261402     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
262290     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
262293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.37ms 
262295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
262295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.41ns 
262296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265077     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
265077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
265993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
265998     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.85ms 
265999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
265999     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84ns 
266000     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
268745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
269673     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
269675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 931.65ns 
269677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
269677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.11ns 
269678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
272448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
272449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
273376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
273380     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 788.74ns 
273385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
273386     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 368.12ns 
273387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
276142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
276143     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
277046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
277049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.56ms 
277051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
277051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.8ns 
277052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279880     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
279881     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
280815     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
280818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 695.64ns 
280820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
280820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 313.62ns 
280822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
283616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
283616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
284540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
284577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.92ms 
284579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
284580     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 254.51ns 
284581     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
287387     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
287387     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
288320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
288347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.73ms 
288349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
288349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.31ns 
288350     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
291176     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
291176     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
292109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
292132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.3ms 
292133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
292133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.91ns 
292134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294882     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
294882     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
295801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
295831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.48ms 
295832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
295832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
295833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
298587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
299507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
299526     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.47ms 
299528     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
299528     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.31ns 
299529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
302311     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
303205     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
303241     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.59ms 
303242     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
303242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.5ns 
303243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
306019     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
306945     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
306963     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.77ms 
306965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
306965     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.2ns 
306966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
309713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
309713     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
310632     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
310646     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.85ms 
310647     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
310647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.91ns 
310648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
313404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
313405     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
314329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
314345     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.95ms 
314346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
314346     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.31ns 
314347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
317098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
317098     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
317966     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
317982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.09ms 
317984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
317984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.31ns 
317985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
320781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
320781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
321693     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
321710     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.75ms 
321711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
321711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86ns 
321712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
324502     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
324502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
325430     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
325447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.59ms 
325449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
325449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.31ns 
325450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
328226     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
328226     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
329109     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
329125     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.91ms 
329127     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
329127     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.11ns 
329128     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
331908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
331909     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
332838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
332854     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.94ms 
332855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
332856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.5ns 
332856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
335577     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
335577     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
336500     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
336516     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.31ms 
336517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
336517     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.8ns 
336518     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
339264     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
339264     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
340194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
340211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.42ms 
340213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
340214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.31ns 
340215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
342984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
343865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
343884     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.74ms 
343885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
343885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.7ns 
343886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346637     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
346637     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
347553     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
347559     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms 
347560     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
347560     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.31ns 
347561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
350303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
351221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
351233     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.19ms 
351235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
351235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
351235     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
353974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
353974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
354909     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
354913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.79ms 
354915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
354915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82ns 
354915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
357689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
357689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
358557     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
358560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 591.23ns 
358561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
358561     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.61ns 
358562     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
361326     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
361326     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
362250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
362253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 743.54ns 
362254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
362254     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.31ns 
362255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
365003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
365003     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
365936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
365941     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.26ms 
365942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
365942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
365943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
368726     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
368727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
369669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
369675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms 
369677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
369677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
369678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
372459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
372459     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
373368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
373379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.36ms 
373381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
373381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
373381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
376139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
376140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
377051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
377054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.65ms 
377055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
377055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
377056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
379762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
379763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
380681     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
380683     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 454.12ns 
380684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
380685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69ns 
380685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
383443     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
383443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
384330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
384335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.95ms 
384336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
384336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.51ns 
384337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
387119     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
387119     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
388044     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
388046     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 574.53ns 
388051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
388051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.41ns 
388052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390816     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
390816     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
391751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
391753     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 535.43ns 
391754     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
391754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
391755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
394515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
394515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
395425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
395427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 565.23ns 
395428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
395428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.1ns 
395429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
398211     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
399113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
399117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
399118     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
399118     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
399119     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
401903     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
401904     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
402824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
402831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.32ms 
402832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
402832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
402833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
405593     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
405593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
406508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
406511     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
406513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
406513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
406513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
409252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
409252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
410160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
410166     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 
410167     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
410167     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.4ns 
410168     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
412941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
412941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
413826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
413835     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.16ms 
413841     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
413841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.21ns 
413843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
416647     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
416647     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
417555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
417572     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.96ms 
417573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
417574     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.3ns 
417574     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
420316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
420317     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
421255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
421259     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.8ms 
421260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
421260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.2ns 
421261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
424036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
424036     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
424930     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
424933     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.04ms 
424935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
424935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74ns 
424936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
427736     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
427736     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
428669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
428673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
428674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
428674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.3ns 
428675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
431425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
431425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
432336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
432350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.97ms 
432351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
432351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
432352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
435104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
435104     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
436033     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
436038     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 363.82ns 
436040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
436041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
436043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
438785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
438785     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
439692     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
439720     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.71ms 
439721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
439721     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.5ns 
439722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
442449     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
442449     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
443365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
443368     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.69ms 
443369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
443369     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.6ns 
443370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
446120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
446120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
447038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
447054     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.25ms 
447055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
447055     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
447056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
449805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
449805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
450724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
450743     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.63ms 
450744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
450744     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.61ns 
450745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
453525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
453525     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
454440     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
454459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.77ms 
454460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
454460     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
454461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
457222     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
457222     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
458108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
458111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 480.93ns 
458112     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
458112     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.9ns 
458113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
460867     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
460867     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
461799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
461804     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.31ms 
461805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
461806     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55.4ns 
461806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
464542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
464542     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
465472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
465476     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
465477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
465477     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
465478     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
468243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
468243     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
469169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
469172     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 777.54ns 
469173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
469173     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.6ns 
469174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
471908     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
471908     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
472834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
472836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 850.75ns 
472838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
472838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 129.11ns 
472839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
475616     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
475616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
476503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
476507     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.34ms 
476508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
476508     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
476509     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
479310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
479310     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
480239     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
480242     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.21ms 
480243     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
480243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
480244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
482984     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
483925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
483934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.72ms 
483935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
483935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
483936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
486761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
487703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
487711     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.12ms 
487716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
487717     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.12ns 
487718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490498     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
490498     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
491443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
491450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.82ms 
491452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
491453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.41ns 
491454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494245     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
494246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
495186     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
495194     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.76ms 
495196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
495196     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77ns 
495196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
497959     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
497959     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
498911     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
498915     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.39ms 
498916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
498916     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
498917     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
501735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
501735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
502656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
502660     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.44ms 
502661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
502661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
502662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
505437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
505438     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
506361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
506364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 759.64ns 
506365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
506366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 203.01ns 
506367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
509125     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
510052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
510055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 976.85ns 
510056     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
510056     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
510057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
512799     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
512799     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
513736     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
513739     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 846.35ns 
513740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
513740     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.1ns 
513741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
516486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
516486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
517418     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
517426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.6ms 
517428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
517428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.6ns 
517428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520163     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
520163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
521071     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
521074     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.28ms 
521075     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
521075     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.9ns 
521076     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523896     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
523896     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
524828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
524833     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.79ms 
524835     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
524835     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.1ns 
524836     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
527606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
528550     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
528552     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 822.04ns 
528555     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
528555     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 228.01ns 
528556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531289     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
531289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
532230     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
532232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 628.23ns 
532233     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
532233     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.5ns 
532238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
535011     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
535956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
535959     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.27ms 
535960     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
535960     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.9ns 
535961     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
538690     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
538691     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
539618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
539624     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 761.74ns 
539625     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
539625     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
539626     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
542425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
543361     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
543364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.13ms 
543366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
543366     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
543367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
546152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
547108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
547111     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.09ms 
547113     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
547113     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.5ns 
547114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
549874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
549875     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
550795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
550800     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
550801     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
550801     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.7ns 
550802     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
553592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
554540     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
554543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 938.05ns 
554544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
554544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
554545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
557322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
558249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
558258     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.93ms 
558259     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
558260     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
558260     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
561002     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
561940     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
561942     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 548.43ns 
561943     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
561943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
561944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564733     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
564733     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
565662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
565668     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms 
565669     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
565669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
565670     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
568432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
569364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
569367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 978.65ns 
569368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
569368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
569369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
572144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
573063     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
573065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 770.24ns 
573066     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
573066     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
573067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
575845     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
576773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
576777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
576778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
576778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.6ns 
576779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579553     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
579554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
580485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
580488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 976.45ns 
580489     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
580489     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
580490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
583262     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
584208     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
584211     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.26ms 
584212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
584212     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
584213     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
586998     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
587920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
587923     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.17ms 
587924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
587924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
587925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
590697     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
591623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
591627     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.32ms 
591629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
591629     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
591629     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
594389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
595321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
595329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.89ms 
595330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
595330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
595331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
598081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
598081     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
599017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
599025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.2ms 
599027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
599027     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
599027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
601749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
602689     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
602696     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.59ms 
602697     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
602697     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.5ns 
602698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605467     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
605467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
606385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
606392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.64ms 
606393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
606393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.91ns 
606394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
609195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
610137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
610150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.95ms 
610152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
610152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 216.81ns 
610153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612930     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
612930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
613862     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
613873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.92ms 
613874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
613874     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.8ns 
613875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616648     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
616648     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
617585     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
617596     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.18ms 
617598     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
617598     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 130.81ns 
617599     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
620365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
621300     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
621307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.09ms 
621308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
621309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.6ns 
621309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
624088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
624088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
625028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
625049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.03ms 
625050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
625050     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
625051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627825     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
627825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
628752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
628781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.43ms 
628784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
628784     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 233.91ns 
628785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
631539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
632473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
632495     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.15ms 
632496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
632496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.5ns 
632497     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
635242     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
635242     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
636173     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
636193     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.07ms 
636195     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
636195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.11ns 
636196     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
638962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
639895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
639913     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.36ms 
639915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
639915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.8ns 
639916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642677     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
642677     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
643610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
643662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.37ms 
643664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
643664     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
643665     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
646408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
646409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
647327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
647332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.7ms 
647333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
647333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 52.6ns 
647334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
650073     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
650073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
651002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
651007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.44ms 
651008     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
651008     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.31ns 
651009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
653763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
654705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
654709     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
654710     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
654711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.3ns 
654711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657454     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
657454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
658366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
658379     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.59ms 
658381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
658381     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.8ns 
658381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661095     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
661095     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
662013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
662024     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.49ms 
662026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
662026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.31ns 
662027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664782     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
664782     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
665718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
665721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
665722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
665722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
665723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668495     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
668495     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
669423     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
669434     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.58ms 
669435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
669436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
669436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
672189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
672189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
673122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
673132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ms 
673133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
673133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
673134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675841     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
675841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
676744     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
676759     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.46ms 
676760     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
676760     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 301.12ns 
676761     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
679538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
680479     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
680482     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.14ms 
680483     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
680483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
680484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
683244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
683244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
684179     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
684183     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.75ms 
684184     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
684184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.1ns 
684185     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
686924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
687844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
687849     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.03ms 
687851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
687851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.1ns 
687851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
690597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
690598     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
691523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
691528     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
691529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
691529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.8ns 
691530     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
694296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
695215     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
695266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.3ms 
695268     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
695268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 183.11ns 
695269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698029     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
698030     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
698974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
698993     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.74ms 
698995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
698995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.9ns 
698996     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
701780     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
702727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
702740     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.42ms 
702741     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
702741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.2ns 
702742     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705533     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
705533     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
706467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
706469     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 175.41ns 
706471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
706471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
706472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
709295     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
710232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
710318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 75.66ms 
710320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
710320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
710321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
713103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
714051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
714088     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.05ms 
714089     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
714090     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.6ns 
714090     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
716851     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
717790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
717792     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 194.61ns 
717795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
717795     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.52ns 
717796     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
720558     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
720559     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
721487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
721489     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 226.61ns 
721490     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
721490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
721491     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
724217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
724218     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
725157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
725159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 227.41ns 
725160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
725160     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 45.7ns 
725161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
727931     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
728868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
728870     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 359.32ns 
728872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
728872     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
728872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
731628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
732556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
732658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 99.32ms 
732659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
732660     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.31ns 
732661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
735431     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
735431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
736347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
736403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 53.34ms 
736404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
736404     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.5ns 
736405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
739140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
739140     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
740060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
740061     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ns 
740094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 49) 
740131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' on goal 3 (script from line 50) 
740145     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' on goal 4 (script from line 51) 
740150     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' on goal 5 (script from line 52) 
740161     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' on goal 11 (script from line 53) 
740162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' on goal 12 (script from line 54) 
740164     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' on goal 13 (script from line 55) 
740166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 14 (script from line 56) 
740170     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' on goal 16 (script from line 58) 
740172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' on goal 17 (script from line 59) 
740174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' on goal 18 (script from line 60) 
740180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' on goal 19 (script from line 61) 
740401     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' on goal 20 (script from line 62) 
740402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' on goal 97 (script from line 63) 
740405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' on goal 98 (script from line 65) 
740405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' on goal 99 (script from line 66) 
740407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' on goal 100 (script from line 67) 
740577     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' on goal 101 (script from line 68) 
740578     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' on goal 188 (script from line 69) 
740581     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' on goal 189 (script from line 71) 
740582     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' on goal 190 (script from line 72) 
740584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' on goal 191 (script from line 73) 
740586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' on goal 192 (script from line 74) 
740801     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' on goal 193 (script from line 75) 
740803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 310 (script from line 76) 
740804     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 311 (script from line 77) 
740805     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' on goal 312 (script from line 79) 
740806     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' on goal 313 (script from line 80) 
740809     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' on goal 314 (script from line 81) 
740974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' on goal 315 (script from line 82) 
740976     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 420 (script from line 83) 
740978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 421 (script from line 84) 
740979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' on goal 422 (script from line 86) 
740980     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' on goal 423 (script from line 87) 
740981     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' on goal 424 (script from line 88) 
740992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' on goal 425 (script from line 89) 
740992     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 434 (script from line 90) 
740995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' on goal 435 (script from line 91) 
740995     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' on goal 436 (script from line 93) 
740997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' on goal 437 (script from line 94) 
740998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' on goal 438 (script from line 95) 
741010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' on goal 439 (script from line 96) 
741011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' on goal 448 (script from line 97) 
741012     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' on goal 449 (script from line 98) 
741013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' on goal 450 (script from line 100) 
741013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' on goal 451 (script from line 101) 
741015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' on goal 452 (script from line 102) 
741244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' on goal 453 (script from line 104) 
741245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' on goal 562 (script from line 105) 
741246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' on goal 563 (script from line 106) 
741427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' on goal 564 (script from line 108) 
741428     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' on goal 674 (script from line 110) 
741430     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' on goal 676 (script from line 112) 
741432     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' on goal 677 (script from line 113) 
741433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' on goal 679 (script from line 114) 
741435     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' on goal 681 (script from line 115) 
741437     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' on goal 683 (script from line 116) 
741438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 685 (script from line 117) 
741443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' on goal 684 (script from line 119) 
741444     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' on goal 687 (script from line 120) 
741446     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' on goal 688 (script from line 121) 
741447     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' on goal 689 (script from line 122) 
741448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' on goal 690 (script from line 123) 
741593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 691 (script from line 124) 
741598     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' on goal 682 (script from line 126) 
741599     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' on goal 796 (script from line 127) 
741601     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' on goal 797 (script from line 128) 
741602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' on goal 798 (script from line 129) 
741602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' on goal 799 (script from line 130) 
741607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' on goal 800 (script from line 131) 
741762     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' on goal 801 (script from line 132) 
741763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' on goal 912 (script from line 133) 
741764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' on goal 913 (script from line 134) 
741766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' on goal 914 (script from line 135) 
741767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' on goal 916 (script from line 136) 
741768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' on goal 917 (script from line 137) 
741770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' on goal 918 (script from line 138) 
741771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' on goal 919 (script from line 139) 
741894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' on goal 920 (script from line 140) 
741896     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' on goal 1011 (script from line 141) 
742020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' on goal 1012 (script from line 142) 
742025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' on goal 915 (script from line 143) 
742032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' on goal 680 (script from line 145) 
742033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' on goal 1099 (script from line 146) 
742035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' on goal 1100 (script from line 147) 
742036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' on goal 1101 (script from line 148) 
742039     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' on goal 1103 (script from line 149) 
742040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' on goal 1104 (script from line 150) 
742040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' on goal 1105 (script from line 151) 
742041     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' on goal 1106 (script from line 152) 
742051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' on goal 1107 (script from line 153) 
742057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' on goal 1102 (script from line 154) 
742189     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' on goal 678 (script from line 156) 
742190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' on goal 1225 (script from line 157) 
742192     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' on goal 1226 (script from line 158) 
742193     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' on goal 1227 (script from line 159) 
742194     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' on goal 1229 (script from line 160) 
742195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' on goal 1230 (script from line 161) 
742195     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' on goal 1231 (script from line 162) 
742196     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' on goal 1232 (script from line 163) 
742262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' on goal 1233 (script from line 164) 
742271     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' on goal 1228 (script from line 165) 
742402     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' on goal 675 (script from line 168) 
742403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' on goal 1397 (script from line 169) 
742405     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' on goal 1399 (script from line 170) 
742407     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' on goal 1400 (script from line 171) 
742408     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' on goal 1401 (script from line 172) 
742409     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' on goal 1402 (script from line 173) 
742580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' on goal 1403 (script from line 174) 
742586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' on goal 1398 (script from line 176) 
742588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' on goal 1534 (script from line 178) 
742590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' on goal 1536 (script from line 180) 
742592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' on goal 1537 (script from line 181) 
742593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' on goal 1539 (script from line 182) 
742594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' on goal 1541 (script from line 183) 
742594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' on goal 1543 (script from line 184) 
742607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' on goal 1544 (script from line 186) 
742613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' on goal 1558 (script from line 187) 
742615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' on goal 1559 (script from line 188) 
742616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' on goal 1560 (script from line 189) 
742749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' on goal 1542 (script from line 191) 
742751     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' on goal 1667 (script from line 192) 
742753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' on goal 1668 (script from line 193) 
742754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' on goal 1669 (script from line 194) 
742754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' on goal 1670 (script from line 195) 
742755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' on goal 1671 (script from line 196) 
742903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' on goal 1672 (script from line 197) 
742905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' on goal 1786 (script from line 198) 
742907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' on goal 1787 (script from line 199) 
742908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' on goal 1788 (script from line 200) 
742909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' on goal 1790 (script from line 201) 
742909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' on goal 1791 (script from line 202) 
742910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' on goal 1792 (script from line 203) 
742911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' on goal 1793 (script from line 204) 
743024     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' on goal 1794 (script from line 205) 
743025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' on goal 1885 (script from line 206) 
743134     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' on goal 1886 (script from line 207) 
743135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' on goal 1968 (script from line 208) 
743136     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' on goal 1969 (script from line 209) 
743142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' on goal 1970 (script from line 210) 
743147     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' on goal 1789 (script from line 211) 
743154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' on goal 1540 (script from line 212) 
743347     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' on goal 1538 (script from line 214) 
743348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' on goal 2097 (script from line 215) 
743349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' on goal 2098 (script from line 216) 
743350     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' on goal 2099 (script from line 217) 
743369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' on goal 2100 (script from line 218) 
743512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' on goal 1535 (script from line 220) 
747724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' on goal 1535 (script from line 223) 
747725     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' on goal 4266 (script from line 225) 
747729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' on goal 4268 (script from line 227) 
747731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' on goal 4269 (script from line 228) 
747732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' on goal 4271 (script from line 229) 
747733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' on goal 4273 (script from line 230) 
747733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' on goal 4275 (script from line 231) 
747742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' on goal 4276 (script from line 233) 
747743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' on goal 4287 (script from line 234) 
747745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' on goal 4288 (script from line 235) 
747746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' on goal 4289 (script from line 236) 
747747     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' on goal 4290 (script from line 237) 
747850     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' on goal 4291 (script from line 238) 
747854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' on goal 4274 (script from line 240) 
747855     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' on goal 4400 (script from line 241) 
747856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' on goal 4401 (script from line 242) 
747857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' on goal 4402 (script from line 243) 
747857     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' on goal 4403 (script from line 244) 
747858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' on goal 4404 (script from line 245) 
747961     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' on goal 4405 (script from line 246) 
747962     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' on goal 4521 (script from line 247) 
747964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' on goal 4522 (script from line 248) 
747965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' on goal 4523 (script from line 249) 
747966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' on goal 4525 (script from line 250) 
747966     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' on goal 4526 (script from line 251) 
747967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' on goal 4527 (script from line 252) 
747968     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' on goal 4528 (script from line 253) 
748053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' on goal 4529 (script from line 254) 
748054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' on goal 4622 (script from line 255) 
748141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' on goal 4623 (script from line 256) 
748146     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' on goal 4524 (script from line 257) 
748151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' on goal 4272 (script from line 259) 
748152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' on goal 4713 (script from line 260) 
748153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' on goal 4714 (script from line 261) 
748154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' on goal 4715 (script from line 262) 
748166     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' on goal 4716 (script from line 263) 
748261     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' on goal 4270 (script from line 265) 
748262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' on goal 4839 (script from line 266) 
748264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' on goal 4840 (script from line 267) 
748264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' on goal 4841 (script from line 268) 
748349     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' on goal 4842 (script from line 269) 
748360     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' on goal 4267 (script from line 272) 
748361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' on goal 4948 (script from line 274) 
748362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' on goal 4950 (script from line 276) 
748363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' on goal 4951 (script from line 277) 
748364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' on goal 4953 (script from line 278) 
748365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' on goal 4955 (script from line 279) 
748365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' on goal 4957 (script from line 280) 
748378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' on goal 4958 (script from line 282) 
748378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' on goal 4977 (script from line 283) 
748379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' on goal 4978 (script from line 284) 
748380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' on goal 4979 (script from line 285) 
748381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' on goal 4980 (script from line 286) 
748486     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' on goal 4981 (script from line 287) 
748487     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' on goal 5093 (script from line 288) 
748489     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' on goal 5094 (script from line 289) 
748490     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' on goal 5095 (script from line 290) 
748491     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' on goal 5096 (script from line 291) 
748642     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' on goal 5097 (script from line 292) 
748647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' on goal 4956 (script from line 294) 
748648     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' on goal 5212 (script from line 295) 
748649     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' on goal 5213 (script from line 296) 
748650     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' on goal 5214 (script from line 299) 
748651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' on goal 5215 (script from line 300) 
748651     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' on goal 5216 (script from line 301) 
748763     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' on goal 5217 (script from line 303) 
748764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' on goal 5337 (script from line 304) 
748765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' on goal 5338 (script from line 305) 
748766     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' on goal 5339 (script from line 306) 
748767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' on goal 5341 (script from line 307) 
748768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' on goal 5342 (script from line 308) 
748768     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' on goal 5343 (script from line 309) 
748769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' on goal 5344 (script from line 310) 
748770     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' on goal 5346 (script from line 311) 
748771     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' on goal 5347 (script from line 312) 
748772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' on goal 5348 (script from line 313) 
748773     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' on goal 5350 (script from line 314) 
748774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' on goal 5351 (script from line 315) 
748774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' on goal 5352 (script from line 316) 
748775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' on goal 5353 (script from line 317) 
748875     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' on goal 5354 (script from line 318) 
748876     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' on goal 5463 (script from line 319) 
748883     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' on goal 5464 (script from line 320) 
748965     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' on goal 5349 (script from line 321) 
749053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' on goal 5345 (script from line 323) 
749055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' on goal 5660 (script from line 324) 
749056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' on goal 5662 (script from line 325) 
749057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' on goal 5663 (script from line 326) 
749058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' on goal 5664 (script from line 327) 
749058     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' on goal 5666 (script from line 328) 
749059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' on goal 5667 (script from line 329) 
749059     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' on goal 5668 (script from line 330) 
749060     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' on goal 5669 (script from line 331) 
749151     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' on goal 5670 (script from line 332) 
749158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' on goal 5665 (script from line 333) 
749254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' on goal 5661 (script from line 335) 
749254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' on goal 5887 (script from line 336) 
749255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' on goal 5888 (script from line 337) 
749256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' on goal 5889 (script from line 338) 
749257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' on goal 5891 (script from line 339) 
749257     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' on goal 5892 (script from line 340) 
749258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' on goal 5893 (script from line 341) 
749258     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' on goal 5894 (script from line 342) 
749264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' on goal 5895 (script from line 343) 
749264     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' on goal 5897 (script from line 344) 
749352     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' on goal 5898 (script from line 345) 
749358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' on goal 5890 (script from line 346) 
749364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' on goal 5340 (script from line 347) 
749470     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' on goal 4954 (script from line 349) 
749471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' on goal 6115 (script from line 350) 
749472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' on goal 6116 (script from line 351) 
749473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' on goal 6117 (script from line 352) 
749473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' on goal 6119 (script from line 353) 
749474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' on goal 6120 (script from line 354) 
749474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' on goal 6121 (script from line 355) 
749474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' on goal 6122 (script from line 356) 
749532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' on goal 6123 (script from line 357) 
749532     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' on goal 6193 (script from line 358) 
749533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' on goal 6195 (script from line 359) 
749534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' on goal 6196 (script from line 360) 
749534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' on goal 6197 (script from line 361) 
749541     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' on goal 6198 (script from line 362) 
749547     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' on goal 6194 (script from line 363) 
749677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' on goal 6118 (script from line 364) 
749775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' on goal 4952 (script from line 366) 
749776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' on goal 6456 (script from line 367) 
749777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' on goal 6457 (script from line 368) 
749778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' on goal 6458 (script from line 369) 
749957     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' on goal 6459 (script from line 370) 
750052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' on goal 4949 (script from line 374) 
750052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' on goal 6735 (script from line 377) 
753433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' on goal 6735 (script from line 379) 
753438     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' on goal 8783 (script from line 380) 
753440     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' on goal 8784 (script from line 381) 
753441     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' on goal 8785 (script from line 382) 
753442     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' on goal 8786 (script from line 383) 
753571     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' on goal 8787 (script from line 384) 
753572     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' on goal 8909 (script from line 385) 
753573     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' on goal 8910 (script from line 386) 
753574     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' on goal 8911 (script from line 387) 
753575     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' on goal 8912 (script from line 388) 
753692     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' on goal 8913 (script from line 389) 
756989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' on goal 6736 (script from line 396) 
760460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' on goal 6736 (script from line 398) 
760464     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' on goal 12633 (script from line 399) 
760466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' on goal 12634 (script from line 400) 
760466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' on goal 12635 (script from line 401) 
760468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' on goal 12636 (script from line 402) 
760591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' on goal 12637 (script from line 403) 
760592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' on goal 12757 (script from line 404) 
760593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' on goal 12758 (script from line 405) 
760594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' on goal 12759 (script from line 406) 
760595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' on goal 12760 (script from line 407) 
761847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
761847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.81ns 
761848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
764638     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
764638     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
765639     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
765640     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 
765640     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 50) 
765647     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' on goal 10 (script from line 51) 
765657     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' on goal 11 (script from line 52) 
765660     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' on goal 12 (script from line 53) 
765662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' on goal 13 (script from line 54) 
765663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' on goal 14 (script from line 55) 
765668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' on goal 15 (script from line 56) 
765668     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' on goal 23 (script from line 57) 
765675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' on goal 27 (script from line 58) 
765675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' on goal 28 (script from line 59) 
765679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' on goal 29 (script from line 60) 
765690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' on goal 30 (script from line 61) 
765690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' on goal 46 (script from line 62) 
765693     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' on goal 47 (script from line 63) 
765741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' on goal 48 (script from line 64) 
765742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' on goal 119 (script from line 65) 
765743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' on goal 120 (script from line 66) 
765744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' on goal 121 (script from line 67) 
765744     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' on goal 122 (script from line 68) 
765818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' on goal 123 (script from line 69) 
765819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' on goal 203 (script from line 70) 
765820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' on goal 204 (script from line 71) 
765821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' on goal 205 (script from line 72) 
765821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' on goal 206 (script from line 73) 
765826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' on goal 207 (script from line 74) 
765826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' on goal 215 (script from line 75) 
765827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' on goal 216 (script from line 76) 
765827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' on goal 217 (script from line 77) 
765828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' on goal 218 (script from line 78) 
765829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' on goal 219 (script from line 79) 
765925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' on goal 220 (script from line 80) 
765926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' on goal 311 (script from line 81) 
765927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' on goal 312 (script from line 82) 
765928     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' on goal 313 (script from line 83) 
765929     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' on goal 314 (script from line 84) 
765930     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' on goal 315 (script from line 85) 
766025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' on goal 316 (script from line 86) 
766025     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' on goal 410 (script from line 87) 
766026     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' on goal 411 (script from line 88) 
766027     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' on goal 412 (script from line 89) 
766028     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' on goal 413 (script from line 90) 
766029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' on goal 414 (script from line 91) 
766029     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' on goal 416 (script from line 92) 
766030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' on goal 417 (script from line 93) 
766031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' on goal 418 (script from line 94) 
766031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' on goal 420 (script from line 95) 
766032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' on goal 421 (script from line 96) 
766032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' on goal 422 (script from line 97) 
766033     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' on goal 423 (script from line 98) 
766034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' on goal 424 (script from line 99) 
766034     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' on goal 425 (script from line 100) 
766035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' on goal 426 (script from line 101) 
766035     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' on goal 427 (script from line 102) 
766036     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' on goal 428 (script from line 103) 
766037     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' on goal 430 (script from line 104) 
766040     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' on goal 431 (script from line 105) 
766083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' on goal 429 (script from line 106) 
766084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' on goal 473 (script from line 107) 
766152     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' on goal 474 (script from line 108) 
766153     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' on goal 541 (script from line 109) 
766154     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' on goal 543 (script from line 110) 
766155     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' on goal 544 (script from line 111) 
766156     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' on goal 545 (script from line 112) 
766158     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' on goal 546 (script from line 113) 
766222     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' on goal 547 (script from line 114) 
766225     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' on goal 542 (script from line 115) 
766226     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' on goal 606 (script from line 116) 
766227     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' on goal 608 (script from line 117) 
766228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' on goal 609 (script from line 118) 
766229     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' on goal 610 (script from line 119) 
766230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' on goal 611 (script from line 120) 
766291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' on goal 612 (script from line 121) 
766294     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' on goal 607 (script from line 122) 
766297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' on goal 419 (script from line 123) 
766364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' on goal 415 (script from line 124) 
766435     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
766435     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.81ns 
766436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
769430     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
769431     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
770469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
770488     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.66ms