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

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

tests
0

failures
0

ignored
13m47.37s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.058s passed
powPositiveConcrete data()[101] 3.872s passed
powGeq1Concrete data()[102] 4.013s passed
pow2InIntLower data()[103] 3.938s passed
pow2InIntUpper data()[104] 4.178s passed
logSelfConcrete data()[105] 4.025s passed
log1Concrete data()[106] 4.078s passed
logProduct data()[107] 3.958s passed
logTimesBaseConcrete data()[108] 3.837s passed
logProdIdentity data()[109] 3.975s passed
moduloByteIsInByte data()[10] 4.165s passed
logProdIdentityConcrete data()[110] 4.072s passed
logPowIdentity data()[111] 4.044s passed
logPowIdentityConcrete data()[112] 3.961s passed
logPositive data()[113] 3.913s passed
logPositiveConcrete data()[114] 4.004s passed
logMono data()[115] 4.020s passed
logMonoConcrete data()[116] 3.852s passed
powLogLess data()[117] 4.012s passed
powLogMore2 data()[118] 4.236s passed
logLessThanPow data()[119] 3.958s passed
moduloCharIsInChar data()[11] 4.154s passed
logLessThanPowConcrete data()[120] 4.010s passed
logSqueeze data()[121] 3.997s passed
ifthenelse_equals data()[122] 4.106s passed
ifthenelse_equals_1 data()[123] 4.069s passed
ifthenelse_equals_2 data()[124] 4.084s passed
disjointWithSingleton1 data()[125] 4.113s passed
disjointWithSingleton2 data()[126] 4.094s passed
disjointArrayRanges data()[127] 4.049s passed
disjointArrayRangeAllFields1 data()[128] 3.858s passed
disjointArrayRangeAllFields2 data()[129] 3.876s passed
div_unique1 data()[12] 4.197s passed
seqSelfDefinition data()[130] 3.892s passed
seqOutsideValue data()[131] 4.119s passed
castedGetAny data()[132] 4.041s passed
seqGetAlphaCast data()[133] 4.155s passed
getOfSeqSingleton data()[134] 4.215s passed
getOfSeqSingletonConcrete data()[135] 4.088s passed
getOfSeqConcat data()[136] 4.117s passed
getOfSeqSub data()[137] 4.130s passed
getOfSeqReverse data()[138] 4.151s passed
lenOfSeqEmpty data()[139] 3.949s passed
div_unique2 data()[13] 4.083s passed
lenOfSeqSingleton data()[140] 4.151s passed
lenOfSeqConcat data()[141] 4.076s passed
lenOfSeqSub data()[142] 4.044s passed
lenOfSeqReverse data()[143] 4.044s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.072s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.991s passed
getOfSeqSingletonEQ data()[146] 4.146s passed
getOfSeqConcatEQ data()[147] 4.161s passed
getOfSeqSubEQ data()[148] 4.223s passed
getOfSeqReverseEQ data()[149] 4.194s passed
div_exists data()[14] 4.243s passed
lenOfSeqEmptyEQ data()[150] 4.152s passed
lenOfSeqSingletonEQ data()[151] 4.106s passed
lenOfSeqConcatEQ data()[152] 3.862s passed
lenOfSeqSubEQ data()[153] 3.882s passed
lenOfSeqReverseEQ data()[154] 4.064s passed
getOfSeqDefEQ data()[155] 4.108s passed
lenOfSeqDefEQ data()[156] 4.093s passed
seqConcatWithSeqEmpty1 data()[157] 4.005s passed
seqConcatWithSeqEmpty2 data()[158] 4.013s passed
seqReverseOfSeqEmpty data()[159] 3.943s passed
div_one data()[15] 4.150s passed
subSeqComplete data()[160] 3.900s passed
subSeqTailR data()[161] 3.969s passed
subSeqTailL data()[162] 4.135s passed
subSeqTailEQR data()[163] 4.000s passed
subSeqTailEQL data()[164] 4.183s passed
seqDef_split data()[165] 4.213s passed
seqDef_induction_upper data()[166] 4.214s passed
seqDef_induction_upper_concrete data()[167] 3.968s passed
seqDef_induction_lower data()[168] 4.005s passed
seqDef_induction_lower_concrete data()[169] 4.044s passed
jdiv_one data()[16] 4.215s passed
seqDef_split_in_three data()[170] 3.979s passed
seqDef_empty data()[171] 3.918s passed
seqDef_one_summand data()[172] 3.882s passed
seqDef_lower_equals_upper data()[173] 3.900s passed
seqDefOfSeq data()[174] 3.962s passed
seqSelfDefinitionEQ2 data()[175] 3.878s passed
indexOfSeqSingleton data()[176] 4.055s passed
indexOfSeqConcatFirst data()[177] 3.985s passed
indexOfSeqConcatSecond data()[178] 3.952s passed
indexOfSeqSub data()[179] 4.200s passed
div_zero data()[17] 4.269s passed
lenOfArray2seq data()[180] 4.105s passed
getAnyOfArray2seq data()[181] 4.066s passed
getOfArray2seq data()[182] 3.891s passed
getAnyOfNPermInv data()[183] 3.882s passed
seqNPermRange data()[184] 3.945s passed
seqPermTrans data()[185] 3.890s passed
seqPermRefl data()[186] 4.019s passed
seqPermSplit data()[187] 4.081s passed
seqNPermRight data()[188] 4.234s passed
seqPermFromSwap data()[189] 4.005s passed
divResZero1 data()[18] 4.129s passed
seqPermTransAlt0 data()[190] 4.141s passed
seqPermTransAlt1 data()[191] 3.919s passed
seqPermTransAlt2 data()[192] 4.095s passed
seqPermTransAlt3 data()[193] 4.062s passed
seqPermForall data()[194] 4.342s passed
seqPermExists data()[195] 4.394s passed
schiffl_lemma_2 data()[196] 25.924s passed
schiffl_thm_1 data()[197] 5.036s passed
eqSameSeq data()[198] 4.016s passed
divResZero2 data()[19] 3.918s passed
eqTermCut data()[1] 5.020s passed
divResOne1 data()[20] 3.921s passed
divResOne2 data()[21] 4.068s passed
div_cancel1 data()[22] 4.097s passed
div_cancel2 data()[23] 3.886s passed
divAddMultDenom data()[24] 4.023s passed
divMinus data()[25] 3.961s passed
divMinusDenom data()[26] 4.134s passed
divLeastDPos data()[27] 3.960s passed
divLeastDNeg data()[28] 3.886s passed
divGreatestDPos data()[29] 3.954s passed
equivAllRight data()[2] 4.858s passed
divGreatestDNeg data()[30] 3.912s passed
divIncreasingPos data()[31] 4.069s passed
divIncreasingNeg data()[32] 4.160s passed
jdiv_zero data()[33] 4.209s passed
jdivPulloutMinusNum data()[34] 4.108s passed
jdivPulloutMinusDenom data()[35] 3.991s passed
jdiv_uniquePosPos data()[36] 3.919s passed
jdiv_uniquePosNeg data()[37] 4.077s passed
jdiv_uniqueNegPos data()[38] 3.919s passed
jdiv_uniqueNegNeg data()[39] 3.926s passed
irrflConcrete1 data()[3] 4.589s passed
jdivMultDenom1 data()[40] 4.137s passed
jdivMultDenom2 data()[41] 3.881s passed
mod_geZero data()[42] 4.186s passed
mod_lessDenom data()[43] 4.225s passed
jmod_NumPos data()[44] 4.259s passed
jmod_NumNeg data()[45] 4.320s passed
jmod_geZero data()[46] 4.073s passed
jmodNumZero data()[47] 4.213s passed
jmod_pulloutminusNum data()[48] 4.081s passed
jmod_pulloutminusDenom data()[49] 4.099s passed
irrflConcrete2 data()[4] 4.326s passed
jmodUnique1 data()[50] 4.158s passed
jmodUnique2 data()[51] 4.172s passed
intDivRem data()[52] 4.024s passed
jmodjmod data()[53] 4.010s passed
jmodDivisible data()[54] 3.944s passed
jmodDivisibleRep data()[55] 3.912s passed
jdivAddMultDenom data()[56] 3.984s passed
jmodAltZero data()[57] 4.045s passed
jmodAddMultDenomZero data()[58] 4.069s passed
polyDiv_zero data()[59] 4.199s passed
cancel_gtPos data()[5] 4.187s passed
polyMod_ltdivDenom data()[60] 4.216s passed
bsum_empty data()[61] 4.072s passed
bsum_induction_upper data()[62] 3.959s passed
bsum_induction_lower data()[63] 4.057s passed
bsum_num_of_bounds data()[64] 4.043s passed
bsum_num_of_bounds2 data()[65] 3.865s passed
bsum_induction_upper2 data()[66] 4.223s passed
bsum_induction_upper_concrete data()[67] 4.128s passed
bsum_induction_upper_concrete_2 data()[68] 4.052s passed
bsum_induction_upper2_concrete data()[69] 4.069s passed
cancel_gtNeg data()[6] 4.091s passed
bsum_induction_lower_concrete data()[70] 4.010s passed
bsum_induction_lower2 data()[71] 3.944s passed
bsum_induction_lower2_concrete data()[72] 4.060s passed
bsum_positive data()[73] 4.202s passed
bsum_upper_bound data()[74] 4.122s passed
bsum_lower_bound data()[75] 3.969s passed
bsum_positive_lower_bound_element data()[76] 4.006s passed
bsum_sub_same_index data()[77] 4.020s passed
bsum_less_same_index data()[78] 4.050s passed
bsum_equal_except_one_index data()[79] 4.006s passed
moduloIntIsInInt data()[7] 4.006s passed
bsum_num_of_is_max data()[80] 3.909s passed
bsum_num_of_is_max2 data()[81] 4.117s passed
bsum_num_of_is_max3 data()[82] 3.881s passed
bsum_num_of_is_max4 data()[83] 3.950s passed
bsum_num_of_lt_max data()[84] 3.957s passed
bsum_num_of_lt_max2 data()[85] 4.047s passed
bsum_num_of_lt_max3 data()[86] 3.998s passed
bsum_num_of_lt_max4 data()[87] 3.848s passed
bsum_num_of_gt0 data()[88] 3.878s passed
bsum_num_of_gt0_alt data()[89] 3.956s passed
moduloLongIsInLong data()[8] 4.112s passed
bsum_add_concrete data()[90] 4.243s passed
bprod_all_positive data()[91] 4.262s passed
bprod_split data()[92] 4.263s passed
powConcrete0 data()[93] 4.109s passed
powConcrete1 data()[94] 4.020s passed
powSplitFactor data()[95] 3.954s passed
powAdd data()[96] 3.901s passed
powMono data()[97] 4.055s passed
powMonoConcrete data()[98] 4.073s passed
powMonoConcreteRight data()[99] 4.019s passed
moduloShortIsInShort data()[9] 4.137s passed

Standard output

952        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
983        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 13.76ms 
1230       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1248       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)

2403       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2415       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2424       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2424       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4036       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
11270      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 10.04s 
11345      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
11392      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.9ns 
11413      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
11413      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 745.91ns 
11421      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
15184      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.76s 
15187      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
16392      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
16420      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.52ms 
16430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
16431      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 582.61ns 
16433      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
20055      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.62s 
20056      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
21259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
21286      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.71ms 
21291      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
21292      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 209.2ns 
21297      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
24715      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.42s 
24716      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
25869      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
25877      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.47ms 
25880      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
25881      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 387.4ns 
25882      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.24s 
29120      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
30189      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
30202      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.02ms 
30210      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
30215      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 5ms 
30217      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33263      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
33264      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
34307      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
34392      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 74.26ms 
34398      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
34399      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 173.8ns 
34400      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37477      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
37477      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
38470      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
38488      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.1ms 
38492      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
38498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 6.45ms 
38500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41484      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
41484      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
42491      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
42495      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 799.41ns 
42498      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
42498      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 410.4ns 
42500      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45587      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
45587      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
46603      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
46607      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 634.91ns 
46609      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
46610      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 407.5ns 
46611      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49663      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
49664      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
50740      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
50744      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 650.31ns 
50750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
50750      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 437.91ns 
50752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
53846      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
53846      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
54909      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
54912      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 643.41ns 
54914      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
54915      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.7ns 
54916      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
58030      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
58031      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
59060      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
59065      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 765.51ns 
59069      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
59069      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 287.2ns 
59070      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
62177      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
62177      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
63223      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
63263      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.6ms 
63274      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
63285      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 11.75ms 
63287      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
66343      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
66343      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
67317      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
67347      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.37ms 
67350      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
67350      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.5ns 
67352      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
70487      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
70487      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
71441      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
71590      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 139.64ms 
71593      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
71594      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 453.11ns 
71595      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
74678      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
74678      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
75736      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
75741      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.87ms 
75743      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
75744      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.8ns 
75745      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78884      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
78885      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
79946      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
79955      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.01ms 
79964      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
79965      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 686.51ns 
79967      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83140      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
83141      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
84181      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
84228      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.85ms 
84233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
84234      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 399.7ns 
84236      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87370      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
87371      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
88347      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
88360      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.98ms 
88362      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
88362      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.4ns 
88363      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
91291      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
91292      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
92266      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
92278      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.61ms 
92280      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
92280      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.1ns 
92282      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
95237      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
96185      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
96199      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.83ms 
96200      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
96201      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.8ns 
96202      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
99196      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
99197      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
100255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
100268     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.08ms 
100269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
100269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.1ns 
100270     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
103343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
103344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
104345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
104364     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.56ms 
104366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
104367     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 344.11ns 
104368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
107278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
107278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
108246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
108250     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.46ms 
108252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
108252     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 302.1ns 
108254     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111268     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
111268     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
112240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
112273     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.9ms 
112275     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
112275     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 118.1ns 
112276     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
115193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
115194     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
116181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
116232     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44.03ms 
116237     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
116237     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.9ns 
116238     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
119303     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
119303     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
120331     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
120369     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.19ms 
120371     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
120371     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 127.9ns 
120372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
123349     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
124322     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
124329     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.93ms 
124330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
124331     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 121.8ns 
124332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127232     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
127233     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
128203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
128215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.04ms 
128217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
128217     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.4ns 
128218     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131188     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
131188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
132158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
132169     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.72ms 
132171     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
132171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.9ns 
132172     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135111     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
135111     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
136068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
136081     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.33ms 
136082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
136083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.2ns 
136087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
139141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
139141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
140141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
140150     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.41ms 
140151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
140151     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104.4ns 
140152     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
143261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
143261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
144302     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
144310     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.91ms 
144312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
144312     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 113.4ns 
144313     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
147525     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.21s 
147527     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
148513     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
148519     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
148523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
148523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 369.9ns 
148524     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
151583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
151583     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
152617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
152628     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.71ms 
152630     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
152630     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 136.5ns 
152631     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
155609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
156578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
156619     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.42ms 
156623     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
156633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 10.68ms 
156635     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
159562     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
159563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
160511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
160538     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.7ms 
160541     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
160542     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.9ns 
160543     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163592     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
163593     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
164589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
164616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.12ms 
164618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
164618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.1ns 
164619     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
167535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
167536     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
168517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
168535     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.51ms 
168536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
168537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.7ns 
168537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
171437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
171437     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
172441     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
172460     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.24ms 
172463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
172463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 331.4ns 
172466     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
175587     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
176561     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
176598     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 31.04ms 
176601     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
176601     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.5ns 
176602     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
179506     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
180474     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
180479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
180481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
180481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94ns 
180482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
183617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
184660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
184664     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.16ms 
184667     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
184667     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 304.91ns 
184668     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
187861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
188881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
188890     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.66ms 
188892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
188892     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 108.8ns 
188893     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
192086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
192086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
193139     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
193149     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.66ms 
193151     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
193153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110.2ns 
193154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
196370     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 
196370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
197446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
197470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.64ms 
197471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
197471     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.6ns 
197472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
200538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
200538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
201533     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
201543     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.74ms 
201544     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
201544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.81ns 
201545     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
204682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
204682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
205751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
205754     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.38ms 
205757     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
205757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 353.81ns 
205758     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
208823     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
208823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
209831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
209836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.89ms 
209837     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
209837     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.5ns 
209838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212921     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
212923     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
213923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
213927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
213939     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
213940     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 339.91ns 
213941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
217014     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
217015     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
218026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
218095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 60.54ms 
218097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
218097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.8ns 
218098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
221159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
221159     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
222169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
222266     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 87.72ms 
222271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
222271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 147.4ns 
222272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
225329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
225329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
226287     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
226293     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.94ms 
226295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
226295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.8ns 
226296     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
229278     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
229278     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
230269     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
230303     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.94ms 
230304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
230305     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.51ns 
230306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
233216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
233217     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
234221     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
234246     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.34ms 
234249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
234249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 320.61ns 
234250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
237221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
237221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
238156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
238159     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.3ms 
238164     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
238164     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.62ns 
238166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
241065     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
241065     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
242024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
242146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 109.33ms 
242149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
242149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.31ns 
242150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
245204     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
245204     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
246175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
246191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.18ms 
246193     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
246193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
246194     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
249252     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
250252     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
250260     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.34ms 
250261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
250262     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 110ns 
250262     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253412     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.15s 
253412     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
254436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
254459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.4ms 
254460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
254461     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.7ns 
254465     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257623     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
257623     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
258655     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
258673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.68ms 
258678     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
258678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 317.71ns 
258679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
261737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
261738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
262743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
262748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.57ms 
262750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
262750     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 266.71ns 
262751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
265738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
265738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
266703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
266707     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.25ms 
266711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
266711     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217.91ns 
266712     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
269714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
269714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
270745     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
270765     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.47ms 
270768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
270768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 166.8ns 
270771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
273824     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
273825     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
274795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
274809     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.43ms 
274811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
274811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
274812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
277725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
277726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
278661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
278675     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.14ms 
278676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
278676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.2ns 
278677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
281820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
281820     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
282888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
282892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
282899     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
282900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 298.71ns 
282901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286001     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
286001     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
287020     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
287025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.29ms 
287026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
287026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
287027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
290078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
291072     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
291078     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.39ms 
291079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
291079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87ns 
291080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
294120     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
294120     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
295143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
295146     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
295147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
295147     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.3ns 
295148     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
298195     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
298195     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
299154     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
299156     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 606.22ns 
299158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
299158     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.6ns 
299158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
302116     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
302116     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
303097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
303101     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
303102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
303102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
303103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
306159     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
306160     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
307158     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
307160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 962.53ns 
307162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
307162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
307163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
310263     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
310263     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
311317     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
311362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.14ms 
311365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
311365     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.11ns 
311366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
314484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
314484     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
315457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
315484     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.19ms 
315486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
315486     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.9ns 
315487     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
318409     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
318409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
319428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
319453     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.52ms 
319455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
319455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.9ns 
319455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
322466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
322467     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
323426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
323459     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 29.17ms 
323461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
323462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 246.51ns 
323463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
326442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
327458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
327479     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.81ms 
327481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
327481     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.3ns 
327482     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
330516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
331486     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
331529     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.64ms 
331531     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
331531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 155.9ns 
331532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334544     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
334545     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
335515     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
335536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.92ms 
335537     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
335537     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 117.8ns 
335538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338424     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
338424     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
339428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
339444     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.02ms 
339446     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
339446     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.7ns 
339447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
342523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
342523     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
343508     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
343560     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.76ms 
343563     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
343563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 255.11ns 
343564     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
346447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
346447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
347426     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
347442     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.42ms 
347444     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
347444     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.3ns 
347445     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
350410     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
350410     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
351369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
351392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.31ms 
351393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
351393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.7ns 
351394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
354333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
354333     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
355330     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
355349     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.46ms 
355351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
355351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.3ns 
355352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
358355     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
358355     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
359376     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
359396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.49ms 
359397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
359397     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.6ns 
359398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
362419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
362419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
363378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
363395     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.02ms 
363396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
363396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 99.2ns 
363397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
366296     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
366296     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
367227     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
367243     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.87ms 
367244     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
367244     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
367245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
370144     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
370144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
371102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
371120     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.54ms 
371122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
371122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.9ns 
371123     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374049     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
374049     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
375057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
375076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.02ms 
375078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
375078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
375079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378281     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
378281     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
379312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
379319     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.69ms 
379320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
379321     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
379321     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
382509     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.19s 
382509     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
383568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
383581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.72ms 
383583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
383583     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
383584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
386785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.2s 
386786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
387839     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
387844     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
387847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
387847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.51ns 
387848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
390962     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
390962     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
391950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
391953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 618.82ns 
391954     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
391954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
391955     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
395007     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
395007     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
395971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
395973     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 801.02ns 
395975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
395975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.1ns 
395975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
398905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
398905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
399921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
399927     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 
399928     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
399929     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
399929     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
402860     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
402860     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
403822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
403828     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.76ms 
403830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
403830     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.3ns 
403831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
406843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
406844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
407872     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
407883     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.89ms 
407885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
407885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
407886     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
410956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
410957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
411953     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
411957     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.04ms 
411958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
411958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.4ns 
411959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414954     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3s 
414955     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
415973     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
415975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 591.41ns 
415976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
415976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
415977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
419043     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
419044     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
420015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
420033     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.61ms 
420035     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
420035     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.91ns 
420036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422925     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
422926     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
423902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
423905     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 626.32ns 
423906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
423906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.1ns 
423907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
426935     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
426935     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
427916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
427919     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 552.41ns 
427920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
427920     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
427921     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
430846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
430846     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
431853     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
431856     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 566.21ns 
431858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
431858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 236.31ns 
431859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
434976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
434976     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
436030     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
436035     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.18ms 
436036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
436036     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
436037     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
439063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
439063     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
440052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
440059     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.39ms 
440064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
440064     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.6ns 
440064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443148     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
443148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
444137     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
444141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.83ms 
444142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
444142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.4ns 
444143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
447132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
448092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
448098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
448099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
448099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.3ns 
448100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
450973     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
450973     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
451931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
451935     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.11ms 
451937     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
451937     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
451938     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
454885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
455896     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
455910     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.41ms 
455912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
455912     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.4ns 
455912     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458974     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
458974     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
459979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
459983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.9ms 
459984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
459984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.5ns 
459985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
463025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
463025     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
464022     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
464026     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
464028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
464028     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
464028     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
466993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
466993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
467983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
467987     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.78ms 
467988     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
467988     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
467989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
470932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
470932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
471885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
471900     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.11ms 
471901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
471902     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
471902     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
474879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
474880     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
475898     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
475903     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 419.41ns 
475906     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
475906     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.7ns 
475907     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
478927     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
478928     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
479894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
479925     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.72ms 
479926     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
479926     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
479927     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
482810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
482810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
483773     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
483777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.63ms 
483778     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
483778     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
483779     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
486751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
486751     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
487768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
487788     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.23ms 
487790     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
487790     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.6ns 
487791     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
490963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
490964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
492007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
492025     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.91ms 
492026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
492026     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
492027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
494995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
494995     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
495962     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
495982     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.28ms 
495984     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
495984     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
495985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498975     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
498975     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
499990     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
499992     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 541.31ns 
499994     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
499994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
499995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502947     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
502947     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
503983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
503990     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.06ms 
503991     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
503991     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
503992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
507088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
507088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
508092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
508095     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.76ms 
508097     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
508097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
508098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
511161     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
511161     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
512161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
512164     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 817.62ns 
512166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
512166     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.7ns 
512166     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
515224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
515225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
516245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
516248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 785.72ns 
516250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
516250     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.4ns 
516250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
519324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
519324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
520357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
520361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
520363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
520363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75ns 
520364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
523484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
523485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
524453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
524456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.25ms 
524457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
524457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
524458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
527475     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
527475     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
528492     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
528503     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.82ms 
528506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
528506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 241.2ns 
528510     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531414     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
531414     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
532355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
532362     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.16ms 
532364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
532364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.8ns 
532365     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
535261     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
536232     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
536239     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.91ms 
536240     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
536240     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.8ns 
536241     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539171     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
539172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
540122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
540130     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.66ms 
540131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
540131     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
540132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
543221     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
543221     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
544245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
544249     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.51ms 
544251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
544251     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 116.3ns 
544251     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
547288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
547289     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
548285     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
548290     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.54ms 
548295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
548295     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.5ns 
548295     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
551372     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
551372     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
552443     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
552446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 797.82ns 
552448     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
552448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.4ns 
552449     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
555590     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
555590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
556659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
556662     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.23ms 
556663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
556663     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73ns 
556664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
559749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
559749     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
560746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
560749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 844.52ns 
560751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
560752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 265.2ns 
560752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
563814     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
563814     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
564856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
564866     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.43ms 
564868     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
564868     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 139.8ns 
564869     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
567952     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
567952     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
568993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
568997     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.41ms 
568998     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
568998     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.2ns 
568999     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
572105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
573141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
573147     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.15ms 
573149     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
573149     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.3ns 
573150     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
576088     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
576088     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
577092     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
577096     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 972.72ns 
577098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
577098     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.1ns 
577098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
580208     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
580208     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
581245     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
581248     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 758.32ns 
581249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
581249     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.5ns 
581250     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
584288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
584288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
585320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
585323     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.43ms 
585325     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
585325     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
585326     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
588390     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
588390     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
589364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
589367     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 870.32ns 
589368     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
589368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.8ns 
589369     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
592376     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
592377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
593409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
593412     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.11ms 
593413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
593413     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
593415     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
596466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
596466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
597481     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
597483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 984.32ns 
597485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
597485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.8ns 
597485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
600440     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
600440     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
601469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
601474     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.5ms 
601475     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
601476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.2ns 
601476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
604581     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
604581     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
605617     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
605620     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 867.32ns 
605621     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
605621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.9ns 
605622     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
608696     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
608696     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
609772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
609781     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.22ms 
609783     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
609783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.9ns 
609784     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612951     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.17s 
612951     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
614002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
614004     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 604.11ns 
614006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
614006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.1ns 
614006     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
617132     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.13s 
617132     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
618192     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
618198     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.02ms 
618200     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
618200     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.5ns 
618201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
621292     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
621292     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
622347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
622350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 934.12ns 
622351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
622351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.4ns 
622352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
625474     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.12s 
625474     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
626454     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
626456     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 813.51ns 
626458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
626458     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.8ns 
626458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
629364     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
629364     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
630314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
630318     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
630320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
630320     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.9ns 
630320     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
633223     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
633223     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
634197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
634200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 911.32ns 
634201     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
634201     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.9ns 
634202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
637235     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
637235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
638261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
638264     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
638266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
638266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56ns 
638266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
641339     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
641339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
642370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
642373     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.12ms 
642374     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
642374     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.6ns 
642375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
645420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
646458     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
646465     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.16ms 
646467     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
646468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 212.3ns 
646469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649483     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
649483     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
650462     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
650470     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.07ms 
650471     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
650472     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
650472     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653490     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
653490     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
654473     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
654483     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ms 
654484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
654485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
654485     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
657468     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
658420     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
658427     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.6ms 
658428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
658428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.2ns 
658429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
661343     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.91s 
661343     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
662319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
662326     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.7ms 
662327     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
662327     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.9ns 
662328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
665258     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
665258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
666284     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
666296     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.82ms 
666297     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
666297     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns 
666298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
669354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
669354     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
670419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
670430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.73ms 
670432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
670432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.6ns 
670433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
673442     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
673443     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
674419     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
674430     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.36ms 
674432     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
674432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.2ns 
674433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
677538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.11s 
677538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
678605     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
678614     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.79ms 
678615     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
678615     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.4ns 
678616     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
681754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.14s 
681754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
682795     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
682826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.54ms 
682828     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
682828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.9ns 
682829     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
685992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
685993     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
687016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
687040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.84ms 
687042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
687042     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.4ns 
687043     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
690006     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.96s 
690006     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
690983     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
691007     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 19.78ms 
691011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
691011     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 238.9ns 
691012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
694018     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
694018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
694993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
695013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.13ms 
695015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
695015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65ns 
695016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
698054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.04s 
698054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
699036     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
699057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.02ms 
699059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
699059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.5ns 
699060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701953     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
701953     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
702978     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
703036     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.76ms 
703038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
703038     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
703039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705971     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.93s 
705971     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
706949     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
706954     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.12ms 
706956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
706956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.2ns 
706956     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
709879     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
709879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
710831     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
710836     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.53ms 
710838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
710838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.9ns 
710838     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
713756     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
713757     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
714732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
714736     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.13ms 
714737     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
714737     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.3ns 
714738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
717656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
717656     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
718684     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
718699     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.65ms 
718701     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
718701     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 225.2ns 
718702     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
721594     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
721594     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
722569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
722576     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.53ms 
722578     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
722578     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 81.2ns 
722579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
725597     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
725597     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
726628     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
726632     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.51ms 
726633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
726633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
726634     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
729628     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.99s 
729628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
730604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
730616     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.27ms 
730618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
730618     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
730618     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
733514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
733514     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
734556     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
734569     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.98ms 
734570     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
734570     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
734571     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
737727     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
737727     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
738752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
738768     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.33ms 
738770     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
738771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 223.1ns 
738771     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
741822     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 
741823     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
742870     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
742873     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.08ms 
742875     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
742875     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 69.1ns 
742876     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
745941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 
745941     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
746936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
746940     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.87ms 
746941     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
746941     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
746942     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
749847     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
749847     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
750824     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
750831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms 
750832     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
750832     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.5ns 
750833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
753732     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.9s 
753732     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
754707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
754712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.09ms 
754714     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
754714     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.4ns 
754715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
757633     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.92s 
757633     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
758610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
758658     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.02ms 
758659     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
758659     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
758660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
761548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.89s 
761549     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
762526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
762547     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.26ms 
762549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
762549     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
762549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765516     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.97s 
765516     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
766554     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
766567     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.34ms 
766568     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
766568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 79.9ns 
766569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
769624     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
769624     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
770644     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
770647     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 185ns 
770649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
770649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 217ns 
770650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
773743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.09s 
773743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
774785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
774881     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.56ms 
774883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
774883     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
774883     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
777866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
777866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
778845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
778886     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.06ms 
778890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
778890     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.2ns 
778891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
781994     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
781994     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
783027     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
783029     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 350.51ns 
783031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
783031     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.3ns 
783031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
785970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
785970     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
786947     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
786949     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 234.5ns 
786950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
786950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
786951     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
789983     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.03s 
789983     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
791041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
791043     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 236.6ns 
791045     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
791045     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.6ns 
791046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
794069     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.02s 
794069     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
795103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
795105     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 404.91ns 
795107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
795107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
795108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
798267     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 
798267     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
799315     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
799434     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
799446     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 128.81ms 
799450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
799450     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 253.9ns 
799451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
802743     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.29s 
802743     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
803794     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
803841     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
803842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.76ms 
803844     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
803844     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.9ns 
803845     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
806949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 
806949     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
807974     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
807976     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.4ns 
808013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
808073     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
808092     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
808099     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
808118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
808120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
808123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
808124     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
808131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
808135     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 17, source line: 59, command: 'instantiate var=iv with='v_x_0' occ=1' 
808138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
808142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
808413     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
808414     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
808417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 98, source line: 64, command: 'instantiate var=iv with='v_y_0' occ=1' 
808418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
808420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
808579     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
808580     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
808583     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
808584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 190, source line: 72, command: 'instantiate var=iv with='v_x_0' occ=2' 
808586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
808589     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
808776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
808778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
808780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
808781     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 312, source line: 78, command: 'instantiate hide var=iv with='v_y_0' occ=2' 
808782     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
808785     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
808967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
808970     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
808971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
808972     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 422, source line: 85, command: 'instantiate var=iv with='jv_0' occ=1' 
808973     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
808974     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
808984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
808985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
808988     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 435, source line: 91, command: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
808989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 436, source line: 92, command: 'instantiate hide var=iv with='jv_1' occ=1' 
808990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
808991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
809002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
809003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
809004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 449, source line: 98, command: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
809005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
809007     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
809008     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
809183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
809184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
809186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
809355     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
809356     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 674, source line: 109, command: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
809358     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
809361     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
809362     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
809363     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
809366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
809367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
809371     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
809373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 687, source line: 120, command: 'instantiate hide var='iv' with='v_x_0' occ=1' 
809374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
809376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
809377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
809515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
809520     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
809522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
809523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
809524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
809525     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
809530     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
809741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
809742     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
809743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
809745     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
809746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
809746     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
809748     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
809749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
809866     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
809868     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
809967     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
809971     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
809978     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
809979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
809982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
809984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
809984     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
809985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
809986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
809986     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
809997     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
810002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
810109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
810110     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
810113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
810114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
810115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
810116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
810118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
810119     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
810177     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
810184     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
810286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [103] goal: 675, source line: 166, command: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
810287     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
810289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [105] goal: 1399, source line: 170, command: 'instantiate hide var=iv with='v_x_0'' 
810290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [106] goal: 1400, source line: 171, command: 'instantiate hide var=jv with='v_y_0'' 
810291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
810292     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
810443     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
810449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [110] goal: 1398, source line: 175, command: 'cut '(int)s_0[v_x_0] = v_x_0'' 
810451     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [111] goal: 1534, source line: 177, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
810453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
810455     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
810456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
810457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
810457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
810468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
810474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [118] goal: 1558, source line: 187, command: 'instantiate hide var=iv with='v_y_0'' 
810476     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
810477     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
810590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
810592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
810593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
810595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
810595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
810596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
810724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
810726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
810728     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
810729     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
810730     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
810731     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
810732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
810732     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
810836     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
810837     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
810925     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
810926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
810927     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
810932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
810936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
810942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
811079     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
811080     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
811081     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
811083     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
811094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
811190     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
815230     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [149] goal: 1535, source line: 221, command: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
815231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [150] goal: 4266, source line: 224, command: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
815236     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
815237     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
815238     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
815240     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
815241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
815250     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
815251     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [157] goal: 4287, source line: 234, command: 'instantiate hide var=iv with='v_x_0'' 
815252     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
815253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
815254     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
815369     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
815373     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
815374     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
815375     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
815377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
815377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
815379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
815492     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
815493     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
815494     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
815495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
815495     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
815496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
815497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
815497     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
815586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
815587     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
815672     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
815677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
815682     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
815683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
815684     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
815686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
815697     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
815790     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
815792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
815793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
815794     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
815878     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
815889     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [190] goal: 4267, source line: 270, command: 'cut '(int)s_0[v_x_0]=v_y_0'' 
815890     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [191] goal: 4948, source line: 273, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
815891     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
815893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
815893     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
815894     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
815895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
815907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
815908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
815909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [199] goal: 4978, source line: 284, command: 'instantiate hide var=jv with='v_x_0'' 
815910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
815911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
816013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [202] goal: 4981, source line: 287, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
816014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
816015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [204] goal: 5094, source line: 289, command: 'instantiate hide var=jv with='v_y_0'' 
816017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
816018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
816123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
816128     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
816129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
816130     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
816131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
816131     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
816132     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
816305     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
816306     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
816307     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
816308     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
816309     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
816310     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
816311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
816311     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
816312     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
816313     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
816314     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
816315     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
816316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
816316     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
816317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
816417     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
816419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
816426     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
816514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
816606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
816607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
816608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
816609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
816610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
816611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
816611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
816611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
816612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
816709     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
816716     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
816818     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
816819     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
816820     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
816821     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
816822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
816822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
816822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
816823     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
816828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
816829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
816920     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
816926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
816932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
817047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
817047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
817048     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
817049     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
817050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
817050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
817050     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
817051     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
817114     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
817115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
817115     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
817116     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
817117     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
817123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
817129     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
817262     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
817364     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
817365     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
817366     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
817367     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
817558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
817661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [278] goal: 4949, source line: 371, command: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
817662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
821104     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
821109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
821111     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [282] goal: 8784, source line: 381, command: 'instantiate hide var=jv with='v_y_0'' 
821112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
821113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
821243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [285] goal: 8787, source line: 384, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
821244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
821245     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [287] goal: 8910, source line: 386, command: 'instantiate hide var=jv with='v_x_0'' 
821246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
821247     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
821368     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
824726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
828326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
828330     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [293] goal: 12633, source line: 399, command: 'instantiate hide var=iv with='v_x_0'' 
828332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
828332     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
828333     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
828465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [297] goal: 12637, source line: 403, command: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
828466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [298] goal: 12757, source line: 404, command: 'instantiate hide var=iv with='v_y_0'' 
828467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
828468     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [300] goal: 12759, source line: 406, command: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
828469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
829767     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
829767     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.1ns 
829768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
833017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.25s 
833017     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
833979     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
833981     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.6ns 
833982     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
833989     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 10, source line: 51, command: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
833999     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
834001     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
834004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
834006     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
834011     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
834013     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
834017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
834017     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
834020     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
834030     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
834031     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
834032     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
834084     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
834094     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
834095     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
834096     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
834097     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
834171     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
834172     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
834173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
834174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
834175     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
834179     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
834180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
834180     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
834181     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
834182     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
834183     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
834277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
834278     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
834279     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
834280     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
834281     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
834282     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
834384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
834387     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
834388     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
834389     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
834390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
834391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
834392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
834393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
834394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
834394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
834395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
834395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
834396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
834396     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
834397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
834398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
834398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
834399     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
834400     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
834403     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
834448     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
834449     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
834517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
834518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
834519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
834521     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
834522     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
834523     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
834584     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
834586     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
834588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
834588     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
834590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
834591     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
834592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
834656     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
834659     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
834663     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
834733     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
834805     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
834805     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.2ns 
834806     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
837745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.94s 
837745     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
838799     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
838818     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.28ms