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

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

tests
0

failures
0

ignored
12m36.37s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.601s passed
powPositiveConcrete data()[101] 3.627s passed
powGeq1Concrete data()[102] 3.693s passed
pow2InIntLower data()[103] 3.653s passed
pow2InIntUpper data()[104] 3.710s passed
logSelfConcrete data()[105] 3.654s passed
log1Concrete data()[106] 3.690s passed
logProduct data()[107] 3.649s passed
logTimesBaseConcrete data()[108] 3.641s passed
logProdIdentity data()[109] 3.633s passed
moduloByteIsInByte data()[10] 3.740s passed
logProdIdentityConcrete data()[110] 3.663s passed
logPowIdentity data()[111] 3.615s passed
logPowIdentityConcrete data()[112] 3.629s passed
logPositive data()[113] 3.638s passed
logPositiveConcrete data()[114] 3.616s passed
logMono data()[115] 3.626s passed
logMonoConcrete data()[116] 3.676s passed
powLogLess data()[117] 3.677s passed
powLogMore2 data()[118] 3.664s passed
logLessThanPow data()[119] 3.665s passed
moduloCharIsInChar data()[11] 3.773s passed
logLessThanPowConcrete data()[120] 3.680s passed
logSqueeze data()[121] 3.647s passed
ifthenelse_equals data()[122] 3.619s passed
ifthenelse_equals_1 data()[123] 3.621s passed
ifthenelse_equals_2 data()[124] 3.636s passed
disjointWithSingleton1 data()[125] 3.673s passed
disjointWithSingleton2 data()[126] 3.638s passed
disjointArrayRanges data()[127] 3.675s passed
disjointArrayRangeAllFields1 data()[128] 3.652s passed
disjointArrayRangeAllFields2 data()[129] 3.665s passed
div_unique1 data()[12] 4.163s passed
seqSelfDefinition data()[130] 3.729s passed
seqOutsideValue data()[131] 3.688s passed
castedGetAny data()[132] 3.695s passed
seqGetAlphaCast data()[133] 3.695s passed
getOfSeqSingleton data()[134] 3.642s passed
getOfSeqSingletonConcrete data()[135] 3.722s passed
getOfSeqConcat data()[136] 3.642s passed
getOfSeqSub data()[137] 3.671s passed
getOfSeqReverse data()[138] 3.654s passed
lenOfSeqEmpty data()[139] 3.664s passed
div_unique2 data()[13] 3.875s passed
lenOfSeqSingleton data()[140] 3.651s passed
lenOfSeqConcat data()[141] 3.661s passed
lenOfSeqSub data()[142] 3.673s passed
lenOfSeqReverse data()[143] 3.670s passed
equalityToSeqGetAndSeqLenLeft data()[144] 3.644s passed
equalityToSeqGetAndSeqLenRight data()[145] 3.666s passed
getOfSeqSingletonEQ data()[146] 3.683s passed
getOfSeqConcatEQ data()[147] 3.638s passed
getOfSeqSubEQ data()[148] 3.613s passed
getOfSeqReverseEQ data()[149] 3.660s passed
div_exists data()[14] 3.837s passed
lenOfSeqEmptyEQ data()[150] 3.665s passed
lenOfSeqSingletonEQ data()[151] 3.666s passed
lenOfSeqConcatEQ data()[152] 3.634s passed
lenOfSeqSubEQ data()[153] 3.677s passed
lenOfSeqReverseEQ data()[154] 3.656s passed
getOfSeqDefEQ data()[155] 3.706s passed
lenOfSeqDefEQ data()[156] 3.709s passed
seqConcatWithSeqEmpty1 data()[157] 3.701s passed
seqConcatWithSeqEmpty2 data()[158] 3.717s passed
seqReverseOfSeqEmpty data()[159] 3.759s passed
div_one data()[15] 3.735s passed
subSeqComplete data()[160] 3.682s passed
subSeqTailR data()[161] 3.689s passed
subSeqTailL data()[162] 3.731s passed
subSeqTailEQR data()[163] 3.671s passed
subSeqTailEQL data()[164] 3.654s passed
seqDef_split data()[165] 3.695s passed
seqDef_induction_upper data()[166] 3.729s passed
seqDef_induction_upper_concrete data()[167] 3.685s passed
seqDef_induction_lower data()[168] 3.719s passed
seqDef_induction_lower_concrete data()[169] 3.700s passed
jdiv_one data()[16] 3.732s passed
seqDef_split_in_three data()[170] 3.727s passed
seqDef_empty data()[171] 3.628s passed
seqDef_one_summand data()[172] 3.670s passed
seqDef_lower_equals_upper data()[173] 3.653s passed
seqDefOfSeq data()[174] 3.775s passed
seqSelfDefinitionEQ2 data()[175] 3.693s passed
indexOfSeqSingleton data()[176] 3.683s passed
indexOfSeqConcatFirst data()[177] 3.673s passed
indexOfSeqConcatSecond data()[178] 3.667s passed
indexOfSeqSub data()[179] 3.706s passed
div_zero data()[17] 3.778s passed
lenOfArray2seq data()[180] 3.657s passed
getAnyOfArray2seq data()[181] 3.623s passed
getOfArray2seq data()[182] 3.702s passed
getAnyOfNPermInv data()[183] 3.698s passed
seqNPermRange data()[184] 3.767s passed
seqPermTrans data()[185] 3.744s passed
seqPermRefl data()[186] 3.727s passed
seqPermSplit data()[187] 3.746s passed
seqNPermRight data()[188] 3.768s passed
seqPermFromSwap data()[189] 3.710s passed
divResZero1 data()[18] 3.686s passed
seqPermTransAlt0 data()[190] 3.634s passed
seqPermTransAlt1 data()[191] 3.695s passed
seqPermTransAlt2 data()[192] 3.653s passed
seqPermTransAlt3 data()[193] 3.668s passed
seqPermForall data()[194] 3.764s passed
seqPermExists data()[195] 3.759s passed
schiffl_lemma_2 data()[196] 26.365s passed
schiffl_thm_1 data()[197] 4.547s passed
eqSameSeq data()[198] 3.929s passed
divResZero2 data()[19] 3.759s passed
eqTermCut data()[1] 4.444s passed
divResOne1 data()[20] 3.728s passed
divResOne2 data()[21] 3.691s passed
div_cancel1 data()[22] 3.764s passed
div_cancel2 data()[23] 3.684s passed
divAddMultDenom data()[24] 3.694s passed
divMinus data()[25] 3.766s passed
divMinusDenom data()[26] 3.701s passed
divLeastDPos data()[27] 3.697s passed
divLeastDNeg data()[28] 3.692s passed
divGreatestDPos data()[29] 3.669s passed
equivAllRight data()[2] 4.078s passed
divGreatestDNeg data()[30] 3.722s passed
divIncreasingPos data()[31] 3.702s passed
divIncreasingNeg data()[32] 3.693s passed
jdiv_zero data()[33] 3.642s passed
jdivPulloutMinusNum data()[34] 3.662s passed
jdivPulloutMinusDenom data()[35] 3.725s passed
jdiv_uniquePosPos data()[36] 3.688s passed
jdiv_uniquePosNeg data()[37] 3.730s passed
jdiv_uniqueNegPos data()[38] 3.693s passed
jdiv_uniqueNegNeg data()[39] 3.718s passed
irrflConcrete1 data()[3] 3.994s passed
jdivMultDenom1 data()[40] 3.666s passed
jdivMultDenom2 data()[41] 3.711s passed
mod_geZero data()[42] 3.683s passed
mod_lessDenom data()[43] 3.681s passed
jmod_NumPos data()[44] 3.772s passed
jmod_NumNeg data()[45] 3.693s passed
jmod_geZero data()[46] 3.715s passed
jmodNumZero data()[47] 3.689s passed
jmod_pulloutminusNum data()[48] 3.722s passed
jmod_pulloutminusDenom data()[49] 3.591s passed
irrflConcrete2 data()[4] 3.869s passed
jmodUnique1 data()[50] 3.776s passed
jmodUnique2 data()[51] 3.787s passed
intDivRem data()[52] 3.660s passed
jmodjmod data()[53] 3.718s passed
jmodDivisible data()[54] 3.665s passed
jmodDivisibleRep data()[55] 3.678s passed
jdivAddMultDenom data()[56] 3.786s passed
jmodAltZero data()[57] 3.673s passed
jmodAddMultDenomZero data()[58] 3.648s passed
polyDiv_zero data()[59] 3.711s passed
cancel_gtPos data()[5] 3.951s passed
polyMod_ltdivDenom data()[60] 3.639s passed
bsum_empty data()[61] 3.673s passed
bsum_induction_upper data()[62] 3.597s passed
bsum_induction_lower data()[63] 3.716s passed
bsum_num_of_bounds data()[64] 3.727s passed
bsum_num_of_bounds2 data()[65] 3.612s passed
bsum_induction_upper2 data()[66] 3.658s passed
bsum_induction_upper_concrete data()[67] 3.605s passed
bsum_induction_upper_concrete_2 data()[68] 3.655s passed
bsum_induction_upper2_concrete data()[69] 3.658s passed
cancel_gtNeg data()[6] 3.862s passed
bsum_induction_lower_concrete data()[70] 3.684s passed
bsum_induction_lower2 data()[71] 3.651s passed
bsum_induction_lower2_concrete data()[72] 3.632s passed
bsum_positive data()[73] 3.650s passed
bsum_upper_bound data()[74] 3.768s passed
bsum_lower_bound data()[75] 3.638s passed
bsum_positive_lower_bound_element data()[76] 3.726s passed
bsum_sub_same_index data()[77] 3.687s passed
bsum_less_same_index data()[78] 3.674s passed
bsum_equal_except_one_index data()[79] 3.689s passed
moduloIntIsInInt data()[7] 3.716s passed
bsum_num_of_is_max data()[80] 3.640s passed
bsum_num_of_is_max2 data()[81] 3.674s passed
bsum_num_of_is_max3 data()[82] 3.637s passed
bsum_num_of_is_max4 data()[83] 3.709s passed
bsum_num_of_lt_max data()[84] 3.718s passed
bsum_num_of_lt_max2 data()[85] 3.777s passed
bsum_num_of_lt_max3 data()[86] 3.716s passed
bsum_num_of_lt_max4 data()[87] 3.724s passed
bsum_num_of_gt0 data()[88] 3.715s passed
bsum_num_of_gt0_alt data()[89] 3.673s passed
moduloLongIsInLong data()[8] 4.026s passed
bsum_add_concrete data()[90] 3.729s passed
bprod_all_positive data()[91] 3.673s passed
bprod_split data()[92] 3.632s passed
powConcrete0 data()[93] 3.622s passed
powConcrete1 data()[94] 3.650s passed
powSplitFactor data()[95] 3.588s passed
powAdd data()[96] 3.665s passed
powMono data()[97] 3.609s passed
powMonoConcrete data()[98] 3.592s passed
powMonoConcreteRight data()[99] 3.610s passed
moduloShortIsInShort data()[9] 3.806s passed

Standard output

769        INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/dummyTrue.key 
797        DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 9.93ms 
1071       INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
1088       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)

2364       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2367       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2372       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
2373       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
4065       DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
10336      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.26s 
10429      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof dummyTrue.key 
10477      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.4ns 
10492      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_eqTermCut.proof 
10492      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 398.9ns 
10497      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
13802      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.3s 
13805      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
14897      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqTermCut 
14925      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.74ms 
14936      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/firstOrder/Taclet_equivAllRight.proof 
14936      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.7ns 
14938      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
18018      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 
18019      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
18997      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equivAllRight 
19012      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.93ms 
19016      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete1.proof 
19016      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.5ns 
19018      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
22028      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 
22029      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
23001      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete1 
23008      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.92ms 
23011      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_irrflConcrete2.proof 
23011      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 530.7ns 
23012      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
25893      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
25894      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
26871      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: irrflConcrete2 
26877      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.76ms 
26881      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtPos.proof 
26882      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 590.2ns 
26883      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
29835      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.95s 
29835      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
30779      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtPos 
30829      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 46.33ms 
30832      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_cancel_gtNeg.proof 
30832      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 153.7ns 
30833      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33702      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.87s 
33702      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
34669      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: cancel_gtNeg 
34692      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.11ms 
34694      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloIntIsInInt.proof 
34695      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149ns 
34696      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
37511      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
37511      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
38404      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloIntIsInInt 
38408      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 999ns 
38421      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloLongIsInLong.proof 
38421      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 505.1ns 
38423      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
41482      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.06s 
41483      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
42438      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloLongIsInLong 
42441      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 663ns 
42444      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloShortIsInShort.proof 
42444      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 335ns 
42446      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
45299      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
45300      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
46236      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloShortIsInShort 
46240      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 778.8ns 
46249      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloByteIsInByte.proof 
46249      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.7ns 
46251      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
49028      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
49028      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
49979      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloByteIsInByte 
49986      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.89ms 
49990      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intRulesIgnoringOF/Taclet_moduloCharIsInChar.proof 
49991      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.3ns 
49993      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
52816      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
52816      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
53758      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: moduloCharIsInChar 
53762      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 647.6ns 
53765      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique1.proof 
53765      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 444.6ns 
53768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
56753      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.98s 
56753      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
57835      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique1 
57925      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 86.04ms 
57927      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_unique2.proof 
57927      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 114.5ns 
57930      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
60790      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.86s 
60791      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
61726      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_unique2 
61797      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 65.61ms 
61805      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_exists.proof 
61806      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 585.8ns 
61809      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
64601      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
64602      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
65521      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_exists 
65637      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 107.21ms 
65641      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_one.proof 
65641      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 361.7ns 
65642      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
68425      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
68425      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
69366      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_one 
69374      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.35ms 
69376      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_one.proof 
69376      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.2ns 
69377      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
72215      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.84s 
72216      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
73102      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_one 
73106      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.45ms 
73110      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_zero.proof 
73110      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 352.3ns 
73111      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
75901      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
75902      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
76812      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_zero 
76884      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 67.4ms 
76889      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero1.proof 
76889      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 314.8ns 
76891      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79672      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
79673      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
80555      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero1 
80572      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.29ms 
80574      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResZero2.proof 
80574      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
80575      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83422      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
83422      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
84317      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResZero2 
84331      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.8ms 
84333      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne1.proof 
84333      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.1ns 
84334      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
87139      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
87139      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
88042      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne1 
88059      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.37ms 
88062      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divResOne2.proof 
88062      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 380.1ns 
88064      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90834      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
90835      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
91734      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divResOne2 
91750      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.45ms 
91752      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel1.proof 
91752      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 149ns 
91753      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
94565      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
94565      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
95481      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel1 
95514      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.17ms 
95516      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_div_cancel2.proof 
95516      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 273.4ns 
95517      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98273      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
98274      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
99194      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: div_cancel2 
99198      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
99200      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divAddMultDenom.proof 
99200      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.9ns 
99201      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
101958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
101958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
102849     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divAddMultDenom 
102892     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.1ms 
102894     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinus.proof 
102894     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
102895     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
105669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
105670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
106593     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinus 
106657     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 56.44ms 
106661     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divMinusDenom.proof 
106661     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.7ns 
106663     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
109419     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
109419     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
110306     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divMinusDenom 
110359     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.46ms 
110366     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDPos.proof 
110368     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.91ms 
110370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
113172     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
113172     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
114050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDPos 
114058     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.27ms 
114060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divLeastDNeg.proof 
114060     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 119.2ns 
114061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
116838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
116838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
117735     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divLeastDNeg 
117750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 12.23ms 
117752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDPos.proof 
117752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 92.7ns 
117753     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120531     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
120531     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
121406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDPos 
121419     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.2ms 
121421     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divGreatestDNeg.proof 
121421     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
121422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
124212     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
125122     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divGreatestDNeg 
125140     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.4ms 
125143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingPos.proof 
125143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106.9ns 
125144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
127924     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
127924     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
128830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingPos 
128842     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.39ms 
128846     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_divIncreasingNeg.proof 
128846     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 131.2ns 
128847     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131617     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
131617     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
132529     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: divIncreasingNeg 
132536     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
132538     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_zero.proof 
132538     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.5ns 
132539     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
135279     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
135279     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
136175     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_zero 
136179     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.74ms 
136180     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusNum.proof 
136180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.2ns 
136181     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
138905     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
138905     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
139823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusNum 
139840     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 14.11ms 
139843     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivPulloutMinusDenom.proof 
139843     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 275.7ns 
139848     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
142621     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
142622     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
143517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivPulloutMinusDenom 
143565     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.95ms 
143567     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosPos.proof 
143568     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 393.5ns 
143569     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
146329     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
146330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
147234     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosPos 
147253     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.66ms 
147255     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniquePosNeg.proof 
147255     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 115.6ns 
147256     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
150074     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
150074     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
150965     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniquePosNeg 
150984     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.91ms 
150985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegPos.proof 
150985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.7ns 
150986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
153765     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
153765     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
154656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegPos 
154676     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.97ms 
154677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdiv_uniqueNegNeg.proof 
154678     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.1ns 
154679     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
157457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
157457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
158375     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdiv_uniqueNegNeg 
158394     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 15.67ms 
158396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom1.proof 
158396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.1ns 
158397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
161125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
161126     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
162018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom1 
162060     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.05ms 
162062     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivMultDenom2.proof 
162063     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 215.4ns 
162064     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
164851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
164852     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
165768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivMultDenom2 
165771     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 973ns 
165776     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_geZero.proof 
165776     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 102ns 
165777     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
168554     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
168554     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
169450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_geZero 
169457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.11ms 
169461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_mod_lessDenom.proof 
169462     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.4ns 
169463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
172243     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
172244     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
173132     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: mod_lessDenom 
173141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.11ms 
173142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumPos.proof 
173143     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 87.9ns 
173144     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
175989     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.85s 
175989     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
176905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumPos 
176914     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.36ms 
176915     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_NumNeg.proof 
176915     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 88.8ns 
176916     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
179694     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
179694     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
180584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_NumNeg 
180606     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 18.59ms 
180608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_geZero.proof 
180608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.8ns 
180609     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
183392     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
183392     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
184311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_geZero 
184321     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.37ms 
184323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodNumZero.proof 
184323     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 96.1ns 
184324     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
187096     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
187096     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
188007     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodNumZero 
188010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.36ms 
188013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusNum.proof 
188013     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 328.5ns 
188014     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
190817     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
190818     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
191727     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusNum 
191732     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
191733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmod_pulloutminusDenom.proof 
191734     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 83.4ns 
191734     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
194436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
194436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
195319     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmod_pulloutminusDenom 
195324     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.63ms 
195332     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique1.proof 
195332     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.9ns 
195333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
198104     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
198105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
199005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique1 
199098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 82.88ms 
199102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodUnique2.proof 
199102     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 349.3ns 
199104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
201899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
201900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
202772     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodUnique2 
202885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 103.36ms 
202888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_intDivRem.proof 
202889     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 267.7ns 
202890     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
205627     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
205627     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
206542     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: intDivRem 
206546     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.71ms 
206548     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodjmod.proof 
206548     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 134.8ns 
206549     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
209322     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
209322     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
210219     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodjmod 
210263     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.43ms 
210266     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisible.proof 
210266     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 418.8ns 
210267     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
212995     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
212996     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
213892     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisible 
213929     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 32.94ms 
213931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodDivisibleRep.proof 
213931     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.2ns 
213934     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
216702     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
216704     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
217604     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodDivisibleRep 
217607     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.19ms 
217608     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jdivAddMultDenom.proof 
217608     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 62.5ns 
217610     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
220330     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
220330     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
221231     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jdivAddMultDenom 
221392     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 150.59ms 
221395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAltZero.proof 
221396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 272.3ns 
221397     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
224155     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
224155     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
225054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAltZero 
225066     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.29ms 
225067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_jmodAddMultDenomZero.proof 
225067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.8ns 
225069     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
227815     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
227815     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
228707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: jmodAddMultDenomZero 
228715     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.81ms 
228716     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyDiv_zero.proof 
228716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.7ns 
228717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
231487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
231487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
232392     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyDiv_zero 
232426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.09ms 
232428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/IntDiv/Taclet_polyMod_ltdivDenom.proof 
232428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 318.5ns 
232429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
235189     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
235189     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
236050     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: polyMod_ltdivDenom 
236065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.44ms 
236067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_empty.proof 
236067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 111.9ns 
236068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
238856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
238856     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
239733     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_empty 
239738     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.27ms 
239739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper.proof 
239739     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.2ns 
239740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
242457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
242457     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
243329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper 
243335     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.36ms 
243336     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower.proof 
243336     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.5ns 
243337     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
246115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
246115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
247024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower 
247049     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.08ms 
247053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds.proof 
247054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 554.4ns 
247055     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
249866     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
249866     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
250724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds 
250777     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 49.67ms 
250781     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_bounds2.proof 
250781     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 245ns 
250782     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
253496     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
253496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
254370     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_bounds2 
254390     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.76ms 
254393     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2.proof 
254393     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 258.9ns 
254394     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
257153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
257153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
258046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2 
258050     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
258051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete.proof 
258051     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 78.5ns 
258052     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
260754     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
260754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
261651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete 
261655     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
261656     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper_concrete_2.proof 
261656     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
261657     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
264417     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
264417     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
265303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper_concrete_2 
265309     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.84ms 
265311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_upper2_concrete.proof 
265311     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 133.3ns 
265312     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
268076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
268077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
268963     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_upper2_concrete 
268967     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.29ms 
268970     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower_concrete.proof 
268970     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 309.8ns 
268972     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
271725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
271726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
272648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower_concrete 
272652     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 760.6ns 
272653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2.proof 
272653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.5ns 
272654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
275420     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
275421     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
276298     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2 
276302     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.37ms 
276303     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_induction_lower2_concrete.proof 
276304     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.4ns 
276304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
279054     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
279054     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
279931     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_induction_lower2_concrete 
279934     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 993.6ns 
279935     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive.proof 
279936     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 146.3ns 
279936     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
282669     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
282670     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
283532     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive 
283584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.87ms 
283587     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_upper_bound.proof 
283587     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 249.3ns 
283589     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
286403     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
286403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
287314     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_upper_bound 
287353     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.5ms 
287354     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_lower_bound.proof 
287354     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.6ns 
287355     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
290105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
290105     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
290959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_lower_bound 
290991     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 28.42ms 
290992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_positive_lower_bound_element.proof 
290992     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.5ns 
290993     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
293771     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
293771     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
294672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_positive_lower_bound_element 
294716     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.49ms 
294717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_sub_same_index.proof 
294718     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.3ns 
294718     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
297453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
297454     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
298372     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_sub_same_index 
298403     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 27.4ms 
298405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_less_same_index.proof 
298405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205.4ns 
298406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
301139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
301139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
302021     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_less_same_index 
302077     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.59ms 
302079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_equal_except_one_index.proof 
302079     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.2ns 
302080     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
304861     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
304861     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
305740     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_equal_except_one_index 
305766     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.97ms 
305768     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max.proof 
305768     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
305769     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
308497     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
308497     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
309387     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max 
309407     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.67ms 
309408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max2.proof 
309408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.4ns 
309409     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
312162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
312162     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
313054     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max2 
313080     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.78ms 
313081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max3.proof 
313081     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
313082     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
315809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
315809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
316698     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max3 
316718     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.32ms 
316719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_is_max4.proof 
316719     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.6ns 
316720     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
319499     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
319499     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
320400     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_is_max4 
320426     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.22ms 
320428     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max.proof 
320428     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 94.8ns 
320429     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
323225     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
323225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
324120     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max 
324145     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.39ms 
324146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max2.proof 
324146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 95.8ns 
324147     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
326963     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.82s 
326964     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
327888     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max2 
327921     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 23.48ms 
327923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max3.proof 
327923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
327925     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
330689     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
330689     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
331582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max3 
331637     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.11ms 
331640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_lt_max4.proof 
331641     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 466.4ns 
331643     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
334439     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
334439     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
335341     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_lt_max4 
335361     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.64ms 
335362     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0.proof 
335363     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.3ns 
335363     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
338156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
338156     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
339048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0 
339076     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.57ms 
339078     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_num_of_gt0_alt.proof 
339078     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 277.6ns 
339079     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
341812     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
341812     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
342729     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_num_of_gt0_alt 
342749     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.81ms 
342751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bsum/Taclet_bsum_add_concrete.proof 
342751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
342752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
345563     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
345563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
346470     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bsum_add_concrete 
346478     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.95ms 
346480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_all_positive.proof 
346480     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
346480     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
349234     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
349235     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
350135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_all_positive 
350151     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.14ms 
350153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/bprod/Taclet_bprod_split.proof 
350153     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
350153     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
352885     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
352885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
353780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: bprod_split 
353784     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
353785     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete0.proof 
353785     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.7ns 
353786     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
356515     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
356515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
357403     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete0 
357406     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 870.2ns 
357407     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powConcrete1.proof 
357407     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
357408     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
360152     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
360152     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
361051     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powConcrete1 
361055     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 882.3ns 
361057     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powSplitFactor.proof 
361057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 205ns 
361058     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
363787     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
363788     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
364637     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powSplitFactor 
364644     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.25ms 
364645     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powAdd.proof 
364645     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.8ns 
364646     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
367396     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
367397     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
368301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powAdd 
368308     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.8ms 
368310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMono.proof 
368310     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.1ns 
368311     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
371041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
371041     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
371905     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMono 
371917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.26ms 
371919     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcrete.proof 
371919     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.1ns 
371920     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
374609     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
374609     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
375505     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcrete 
375509     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.19ms 
375511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powMonoConcreteRight.proof 
375511     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.8ns 
375511     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
378241     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
378241     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
379117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powMonoConcreteRight 
379119     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 707ns 
379121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositive.proof 
379121     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.2ns 
379121     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
381840     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
381841     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
382715     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositive 
382721     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.95ms 
382722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powPositiveConcrete.proof 
382722     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.2ns 
382723     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
385441     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
385442     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
386345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powPositiveConcrete 
386347     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 674.5ns 
386349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powGeq1Concrete.proof 
386349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132ns 
386349     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
389115     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
389115     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
390038     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powGeq1Concrete 
390040     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 592.09ns 
390041     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntLower.proof 
390041     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.7ns 
390042     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
392786     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
392786     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
393691     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntLower 
393694     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 570.8ns 
393695     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_pow2InIntUpper.proof 
393695     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.8ns 
393696     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
396491     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
396491     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
397399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: pow2InIntUpper 
397404     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.06ms 
397405     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSelfConcrete.proof 
397405     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.4ns 
397406     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
400141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
400141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
401048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSelfConcrete 
401057     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.66ms 
401059     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_log1Concrete.proof 
401059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
401060     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
403836     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
403837     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
404743     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: log1Concrete 
404747     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
404749     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProduct.proof 
404749     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.3ns 
404750     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
407514     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
407515     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
408390     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProduct 
408396     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.1ms 
408398     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logTimesBaseConcrete.proof 
408398     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 59.2ns 
408399     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
411122     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
411122     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
412031     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logTimesBaseConcrete 
412037     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.38ms 
412039     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentity.proof 
412039     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.2ns 
412040     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
414763     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
414763     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
415654     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentity 
415670     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.03ms 
415671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logProdIdentityConcrete.proof 
415671     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 101.7ns 
415672     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
418466     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
418466     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
419329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logProdIdentityConcrete 
419333     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.23ms 
419334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentity.proof 
419334     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.3ns 
419335     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
422052     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
422052     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
422944     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentity 
422948     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.39ms 
422950     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPowIdentityConcrete.proof 
422950     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
422952     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
425680     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
425680     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
426573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPowIdentityConcrete 
426577     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.14ms 
426579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositive.proof 
426579     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.8ns 
426579     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
429324     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
429324     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
430197     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositive 
430215     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.96ms 
430216     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logPositiveConcrete.proof 
430216     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.3ns 
430217     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
432942     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
432943     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
433826     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logPositiveConcrete 
433831     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 345.8ns 
433833     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMono.proof 
433833     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 65.6ns 
433834     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
436527     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.69s 
436528     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
437422     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMono 
437457     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 30.84ms 
437459     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logMonoConcrete.proof 
437459     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.3ns 
437460     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
440214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
440214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
441130     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logMonoConcrete 
441133     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.72ms 
441135     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogLess.proof 
441135     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 104ns 
441136     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
443913     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
443913     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
444789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogLess 
444810     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.28ms 
444811     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_powLogMore2.proof 
444811     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.1ns 
444812     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
447556     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
447556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
448455     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: powLogMore2 
448475     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 17.05ms 
448476     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPow.proof 
448476     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.4ns 
448477     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
451229     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
451229     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
452114     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPow 
452139     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.63ms 
452141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logLessThanPowConcrete.proof 
452141     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.3ns 
452141     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
454918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
454919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
455816     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logLessThanPowConcrete 
455819     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 828.8ns 
455820     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/intPow/Taclet_logSqueeze.proof 
455820     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
455821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
458567     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
458567     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
459461     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: logSqueeze 
459467     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.09ms 
459468     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals.proof 
459468     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.2ns 
459469     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
462184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
462185     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
463081     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals 
463085     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.97ms 
463086     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_1.proof 
463086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.3ns 
463087     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
465810     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
465810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
466703     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_1 
466706     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
466707     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/booleanRules/Taclet_ifthenelse_equals_2.proof 
466707     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 57.2ns 
466708     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
469455     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
469455     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
470340     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: ifthenelse_equals_2 
470342     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 789.1ns 
470345     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton1.proof 
470345     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.6ns 
470346     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
473105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
473106     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
474013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton1 
474016     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.4ms 
474017     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointWithSingleton2.proof 
474017     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
474018     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
476725     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
476726     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
477649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointWithSingleton2 
477654     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.42ms 
477662     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRanges.proof 
477662     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 383.4ns 
477664     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
480425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
480425     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
481323     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRanges 
481332     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.56ms 
481333     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields1.proof 
481333     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 124.2ns 
481334     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
484076     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
484077     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
484975     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields1 
484983     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.42ms 
484985     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/locSet/Taclet_disjointArrayRangeAllFields2.proof 
484985     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58ns 
484986     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
487730     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
487730     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
488640     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: disjointArrayRangeAllFields2 
488649     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.48ms 
488650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinition.proof 
488650     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 66.7ns 
488651     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
491448     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.8s 
491448     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
492364     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinition 
492377     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.09ms 
492380     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqOutsideValue.proof 
492380     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 231.3ns 
492381     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
495140     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
495141     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
496061     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqOutsideValue 
496065     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.34ms 
496067     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_castedGetAny.proof 
496067     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.6ns 
496068     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
498809     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
498809     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
499755     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: castedGetAny 
499760     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.1ms 
499762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqGetAlphaCast.proof 
499762     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
499762     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
502529     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
502529     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
503453     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqGetAlphaCast 
503455     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 875.4ns 
503457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingleton.proof 
503457     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.7ns 
503457     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
506179     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
506179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
507094     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingleton 
507097     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.53ms 
507098     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonConcrete.proof 
507099     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 206.2ns 
507100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
509893     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
509893     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
510817     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonConcrete 
510820     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.24ms 
510821     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcat.proof 
510821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.6ns 
510822     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
513539     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
513539     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
514450     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcat 
514461     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.63ms 
514463     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSub.proof 
514463     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 75.8ns 
514464     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
517205     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
517205     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
518129     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSub 
518132     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.49ms 
518133     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverse.proof 
518133     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.8ns 
518134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
520870     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
520870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
521780     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverse 
521787     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.34ms 
521788     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmpty.proof 
521788     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.3ns 
521789     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
524522     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
524522     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
525447     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmpty 
525450     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 823.3ns 
525451     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingleton.proof 
525452     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 162.9ns 
525452     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
528181     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
528181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
529099     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingleton 
529102     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 721.6ns 
529103     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcat.proof 
529103     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 73.6ns 
529104     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
531838     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
531838     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
532759     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcat 
532763     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.59ms 
532764     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSub.proof 
532764     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.1ns 
532765     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
535513     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
535513     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
536433     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSub 
536435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 965.7ns 
536436     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverse.proof 
536437     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.7ns 
536437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
539187     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
539188     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
540102     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverse 
540106     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.44ms 
540107     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenLeft.proof 
540107     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 72.7ns 
540108     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
542826     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
542826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
543747     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenLeft 
543750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 982.1ns 
543751     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_equalityToSeqGetAndSeqLenRight.proof 
543751     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 106ns 
543752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
546500     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
546500     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
547411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: equalityToSeqGetAndSeqLenRight 
547415     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.42ms 
547416     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSingletonEQ.proof 
547416     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 54.7ns 
547417     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
550180     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
550181     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
551096     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSingletonEQ 
551098     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.18ms 
551100     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqConcatEQ.proof 
551100     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 53.3ns 
551101     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
553821     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
553821     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
554726     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqConcatEQ 
554737     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.84ms 
554738     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqSubEQ.proof 
554738     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 84.3ns 
554739     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
557436     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
557436     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
558347     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqSubEQ 
558350     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 715.6ns 
558351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqReverseEQ.proof 
558351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
558352     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
561068     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
561068     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
562001     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqReverseEQ 
562010     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.3ms 
562012     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqEmptyEQ.proof 
562012     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 226.6ns 
562013     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
564758     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
564758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
565671     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqEmptyEQ 
565674     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.01ms 
565676     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSingletonEQ.proof 
565676     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 89.2ns 
565677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
568423     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
568423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
569338     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSingletonEQ 
569340     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 803.3ns 
569342     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqConcatEQ.proof 
569342     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
569343     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
572062     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
572062     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
572971     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqConcatEQ 
572975     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.03ms 
572976     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqSubEQ.proof 
572976     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 126.5ns 
572977     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
575735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
575735     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
576648     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqSubEQ 
576651     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.15ms 
576652     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqReverseEQ.proof 
576653     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
576653     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
579389     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
579389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
580304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqReverseEQ 
580307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.55ms 
580309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfSeqDefEQ.proof 
580309     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
580310     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
583086     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
583086     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
584009     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfSeqDefEQ 
584013     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.52ms 
584015     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfSeqDefEQ.proof 
584015     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.9ns 
584016     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
586803     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
586803     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
587719     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfSeqDefEQ 
587723     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.38ms 
587724     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty1.proof 
587724     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.9ns 
587725     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
590503     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
590503     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
591414     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty1 
591423     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.11ms 
591425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqConcatWithSeqEmpty2.proof 
591425     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.9ns 
591425     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
594214     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
594214     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
595131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqConcatWithSeqEmpty2 
595141     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.81ms 
595142     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqReverseOfSeqEmpty.proof 
595142     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.7ns 
595143     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
597956     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
597956     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
598891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqReverseOfSeqEmpty 
598899     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.79ms 
598900     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqComplete.proof 
598900     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.2ns 
598901     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
601666     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
601666     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
602573     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqComplete 
602581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.5ms 
602582     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailR.proof 
602582     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 61.1ns 
602583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
605347     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
605348     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
606258     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailR 
606270     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.82ms 
606271     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailL.proof 
606271     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.2ns 
606272     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
609057     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
609057     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
609989     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailL 
610002     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.19ms 
610003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQR.proof 
610003     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 82.9ns 
610004     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
612761     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
612761     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
613660     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQR 
613673     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.92ms 
613674     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_subSeqTailEQL.proof 
613674     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
613675     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
616383     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
616383     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
617318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: subSeqTailEQL 
617327     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.52ms 
617328     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split.proof 
617328     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80ns 
617329     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
620059     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
620059     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
620995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split 
621021     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 22.63ms 
621023     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper.proof 
621023     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.9ns 
621024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
623792     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
623792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
624722     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper 
624750     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 24.1ms 
624752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_upper_concrete.proof 
624752     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64.7ns 
624752     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
627485     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
627485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
628395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_upper_concrete 
628435     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 35.62ms 
628437     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower.proof 
628438     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 271.4ns 
628439     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
631224     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.79s 
631224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
632131     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower 
632154     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 20.38ms 
632156     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_induction_lower_concrete.proof 
632156     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60ns 
632157     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
634918     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
634919     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
635830     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_induction_lower_concrete 
635855     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 21.13ms 
635856     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_split_in_three.proof 
635856     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 55ns 
635857     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
638603     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
638603     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
639517     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_split_in_three 
639581     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.57ms 
639583     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_empty.proof 
639584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 261.5ns 
639584     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
642298     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.71s 
642298     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
643203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_empty 
643209     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.74ms 
643211     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_one_summand.proof 
643211     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.2ns 
643212     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
645958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
645958     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
646873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_one_summand 
646879     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.99ms 
646880     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDef_lower_equals_upper.proof 
646881     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.6ns 
646881     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
649606     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
649606     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
650526     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDef_lower_equals_upper 
650533     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 5.04ms 
650535     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqDefOfSeq.proof 
650535     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 192.1ns 
650536     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
653344     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.81s 
653344     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
654289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqDefOfSeq 
654307     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.81ms 
654308     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqSelfDefinitionEQ2.proof 
654308     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.2ns 
654309     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
657083     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
657084     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
657992     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqSelfDefinitionEQ2 
658001     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 6.11ms 
658002     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSingleton.proof 
658002     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 56.4ns 
658003     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
660757     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
660758     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
661680     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSingleton 
661684     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.95ms 
661685     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatFirst.proof 
661685     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 60.4ns 
661686     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
664432     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
664432     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
665344     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatFirst 
665356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.74ms 
665357     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqConcatSecond.proof 
665357     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 58.6ns 
665358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
668097     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
668097     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
669011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqConcatSecond 
669023     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.52ms 
669024     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_indexOfSeqSub.proof 
669025     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 77.1ns 
669026     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
671794     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
671794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
672713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: indexOfSeqSub 
672729     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 13.7ms 
672731     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_lenOfArray2seq.proof 
672731     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 76.9ns 
672732     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
675453     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.72s 
675453     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
676384     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: lenOfArray2seq 
676387     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 1.03ms 
676388     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getAnyOfArray2seq.proof 
676388     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 135.6ns 
676389     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
679092     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.7s 
679093     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
680005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfArray2seq 
680009     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 2.07ms 
680010     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_getOfArray2seq.proof 
680010     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 100.4ns 
680011     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
682783     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
682784     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
683705     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getOfArray2seq 
683712     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.92ms 
683713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_getAnyOfNPermInv.proof 
683713     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 63.8ns 
683713     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
686487     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
686487     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
687404     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: getAnyOfNPermInv 
687410     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 3.45ms 
687411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqNPermRange.proof 
687411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 103.4ns 
687412     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
690193     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.78s 
690193     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
691117     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRange 
691176     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 52.79ms 
691178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTrans.proof 
691178     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 80.5ns 
691178     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
693948     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
693948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
694885     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTrans 
694920     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 26.47ms 
694923     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermRefl.proof 
694923     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 199.5ns 
694924     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
697682     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
697682     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
698633     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermRefl 
698648     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 11.64ms 
698649     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermSplit.proof 
698649     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 67.7ns 
698650     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
701408     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
701409     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
702391     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermSplit 
702393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 242.5ns 
702395     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_seqNPermRight.proof 
702395     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
702396     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
705138     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
705138     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
706053     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqNPermRight 
706160     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 95.4ms 
706162     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermFromSwap.proof 
706162     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 74.3ns 
706163     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
708899     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
708900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
709825     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermFromSwap 
709871     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.28ms 
709873     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt0.proof 
709873     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 51.2ns 
709874     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
712599     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
712599     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
713503     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt0 
713505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 261.7ns 
713506     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt1.proof 
713506     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 50.5ns 
713507     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
716269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.76s 
716270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
717198     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt1 
717200     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 263.9ns 
717202     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt2.proof 
717202     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 71.7ns 
717203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
719932     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
719932     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
720851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt2 
720853     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 483.4ns 
720854     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermTransAlt3.proof 
720854     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 49.8ns 
720855     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
723584     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.73s 
723584     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
724519     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermTransAlt3 
724521     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 402ns 
724523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermForall.proof 
724523     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 156.6ns 
724523     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
727269     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.75s 
727270     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermForall 
728174     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermForall 
728273     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_4) 
728285     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 105ms 
728288     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm/Taclet_seqPermExists.proof 
728288     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 242.6ns 
728289     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
731058     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.77s 
731058     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermExists 
731995     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: seqPermExists 
732043     INFO  Test worker     d.u.i.k.s.SMTFocusResults Analyzing unsat core: (L_1 L_3 L_5 L_6 L_7) 
732044     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 47.07ms 
732046     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_lemma_2.proof 
732046     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 64ns 
732048     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
734791     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.74s 
734792     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
735746     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_lemma_2 
735748     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 4.3ns 
735786     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 49, command: 'macro split-prop' 
735822     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 50, command: 'rule allRight' 
735838     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 4, source line: 51, command: 'rule allRight' 
735843     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 5, source line: 52, command: 'macro split-prop' 
735854     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 11, source line: 53, command: 'rule 'seqPermDefLeft'' 
735856     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 12, source line: 54, command: 'rule 'andLeft'' 
735858     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 13, source line: 55, command: 'rule 'exLeft'' 
735859     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 14, source line: 56, command: 'macro split-prop' 
735864     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 16, source line: 57, command: 'rule  seqNPermRange' 
735865     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' 
735867     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 18, source line: 60, command: 'rule impLeft' 
735870     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 19, source line: 61, command: 'tryclose branch' 
736086     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 20, source line: 62, command: 'rule andLeft' 
736088     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 97, source line: 63, command: 'rule andLeft' 
736089     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' 
736090     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 99, source line: 66, command: 'rule impLeft' 
736091     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 100, source line: 67, command: 'tryclose branch' 
736244     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 101, source line: 68, command: 'rule andLeft' 
736246     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 188, source line: 69, command: 'rule andLeft' 
736249     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 189, source line: 70, command: 'rule seqNPermDefLeft' 
736251     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' 
736253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 191, source line: 73, command: 'rule impLeft' 
736256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 192, source line: 74, command: 'tryclose branch' 
736513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 193, source line: 75, command: 'rule exLeft' 
736516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 310, source line: 76, command: 'rule andLeft' 
736517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 311, source line: 77, command: 'rule andLeft' 
736518     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' 
736524     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 313, source line: 80, command: 'rule impLeft' 
736527     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 314, source line: 81, command: 'tryclose branch' 
736715     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 315, source line: 82, command: 'rule exLeft' 
736719     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 420, source line: 83, command: 'rule andLeft' 
736720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 421, source line: 84, command: 'rule andLeft' 
736721     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' 
736722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 423, source line: 87, command: 'rule impLeft' 
736724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 424, source line: 88, command: 'tryclose branch' 
736734     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 425, source line: 89, command: 'rule andLeft' 
736735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 434, source line: 90, command: 'rule andLeft' 
736738     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' 
736739     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' 
736741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 437, source line: 94, command: 'rule impLeft' 
736743     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 438, source line: 95, command: 'tryclose branch' 
736760     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 439, source line: 96, command: 'rule andLeft' 
736761     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 448, source line: 97, command: 'rule andLeft' 
736762     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' 
736764     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 450, source line: 99, command: 'instantiate var=iv  with='v_x_0'' 
736765     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 451, source line: 101, command: 'rule impLeft' 
736767     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 452, source line: 102, command: 'tryclose branch' 
736942     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 453, source line: 103, command: 'instantiate var=iv  with='v_y_0'' 
736943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 562, source line: 105, command: 'rule impLeft' 
736945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 563, source line: 106, command: 'tryclose branch' 
737102     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 564, source line: 107, command: 'cut 'v_x_0 = v_y_0'' 
737103     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)'' 
737105     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 676, source line: 111, command: 'rule andRight' 
737107     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 677, source line: 113, command: 'rule andRight' 
737109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 679, source line: 114, command: 'rule andRight' 
737109     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 681, source line: 115, command: 'rule andRight' 
737112     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 683, source line: 116, command: 'rule lenOfSwap' 
737113     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 685, source line: 117, command: 'tryclose branch' 
737118     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 684, source line: 118, command: 'rule seqNPermSwapNPerm' 
737120     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' 
737121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 688, source line: 121, command: 'instantiate hide var='jv' with='jv_0'' 
737122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 689, source line: 122, command: 'rule impLeft' 
737123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 690, source line: 123, command: 'tryclose branch' 
737277     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 691, source line: 124, command: 'tryclose branch' 
737286     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 682, source line: 125, command: 'rule allRight' 
737288     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 796, source line: 127, command: 'rule impRight' 
737289     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 797, source line: 128, command: 'rule andLeft' 
737290     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 798, source line: 129, command: 'instantiate var=iv with='v_iv_0'' 
737291     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 799, source line: 130, command: 'rule impLeft' 
737298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 800, source line: 131, command: 'tryclose branch' 
737466     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 801, source line: 132, command: 'rule getOfSwap' 
737467     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 912, source line: 133, command: 'rule ifthenelse_negated' 
737469     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 913, source line: 134, command: 'rule ifthenelse_split occ=0' 
737471     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 914, source line: 135, command: 'rule andLeft' 
737472     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 916, source line: 136, command: 'rule andLeft' 
737473     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [76] goal: 917, source line: 137, command: 'rule andLeft' 
737474     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [77] goal: 918, source line: 138, command: 'rule ifthenelse_split occ=0' 
737475     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [78] goal: 919, source line: 139, command: 'tryclose branch' 
737610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [79] goal: 920, source line: 140, command: 'rule ifthenelse_split occ=0' 
737611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [80] goal: 1011, source line: 141, command: 'tryclose branch' 
737735     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [81] goal: 1012, source line: 142, command: 'tryclose branch' 
737741     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [82] goal: 915, source line: 143, command: 'tryclose branch' 
737749     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [83] goal: 680, source line: 144, command: 'rule getOfSwap' 
737750     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [84] goal: 1099, source line: 146, command: 'rule ifthenelse_negated' 
737754     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [85] goal: 1100, source line: 147, command: 'rule ifthenelse_split occ=0' 
737755     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [86] goal: 1101, source line: 148, command: 'rule andLeft' 
737756     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [87] goal: 1103, source line: 149, command: 'rule andLeft' 
737757     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [88] goal: 1104, source line: 150, command: 'rule andLeft' 
737758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [89] goal: 1105, source line: 151, command: 'rule ifthenelse_split occ=0' 
737758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [90] goal: 1106, source line: 152, command: 'tryclose branch' 
737769     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [91] goal: 1107, source line: 153, command: 'tryclose branch' 
737775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [92] goal: 1102, source line: 154, command: 'tryclose branch' 
737902     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [93] goal: 678, source line: 155, command: 'rule getOfSwap' 
737903     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [94] goal: 1225, source line: 157, command: 'rule ifthenelse_negated' 
737905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [95] goal: 1226, source line: 158, command: 'rule ifthenelse_split occ=0' 
737907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [96] goal: 1227, source line: 159, command: 'rule andLeft' 
737908     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [97] goal: 1229, source line: 160, command: 'rule andLeft' 
737909     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [98] goal: 1230, source line: 161, command: 'rule andLeft' 
737910     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [99] goal: 1231, source line: 162, command: 'rule ifthenelse_split occ=0' 
737911     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [100] goal: 1232, source line: 163, command: 'tryclose branch' 
737977     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [101] goal: 1233, source line: 164, command: 'tryclose branch' 
737985     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [102] goal: 1228, source line: 165, command: 'tryclose branch' 
738137     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]'' 
738138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [104] goal: 1397, source line: 169, command: 'rule seqNPermInjective' 
738139     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'' 
738141     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'' 
738142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [107] goal: 1401, source line: 172, command: 'rule impLeft' 
738144     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [108] goal: 1402, source line: 173, command: 'tryclose branch' 
738317     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [109] goal: 1403, source line: 174, command: 'tryclose branch' 
738322     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'' 
738323     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)'' 
738324     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [112] goal: 1536, source line: 179, command: 'rule andRight' 
738325     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [113] goal: 1537, source line: 181, command: 'rule andRight' 
738326     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [114] goal: 1539, source line: 182, command: 'rule andRight' 
738327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [115] goal: 1541, source line: 183, command: 'rule andRight' 
738327     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [116] goal: 1543, source line: 184, command: 'tryclose branch' 
738338     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [117] goal: 1544, source line: 185, command: 'rule seqNPermSwapNPerm' 
738339     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'' 
738340     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [119] goal: 1559, source line: 188, command: 'instantiate hide var=jv with='jv_1'' 
738341     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [120] goal: 1560, source line: 189, command: 'tryclose branch' 
738456     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [121] goal: 1542, source line: 190, command: 'rule allRight' 
738457     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [122] goal: 1667, source line: 192, command: 'rule impRight' 
738458     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [123] goal: 1668, source line: 193, command: 'rule andLeft' 
738459     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [124] goal: 1669, source line: 194, command: 'instantiate var=iv with='v_iv_0'' 
738460     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [125] goal: 1670, source line: 195, command: 'rule impLeft' 
738461     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [126] goal: 1671, source line: 196, command: 'tryclose branch' 
738590     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [127] goal: 1672, source line: 197, command: 'rule getOfSwap' 
738592     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [128] goal: 1786, source line: 198, command: 'rule ifthenelse_negated' 
738593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [129] goal: 1787, source line: 199, command: 'rule ifthenelse_split occ=0' 
738594     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [130] goal: 1788, source line: 200, command: 'rule andLeft' 
738595     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [131] goal: 1790, source line: 201, command: 'rule andLeft' 
738596     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [132] goal: 1791, source line: 202, command: 'rule andLeft' 
738602     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [133] goal: 1792, source line: 203, command: 'rule ifthenelse_split occ=0' 
738603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [134] goal: 1793, source line: 204, command: 'tryclose branch' 
738700     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [135] goal: 1794, source line: 205, command: 'rule ifthenelse_split occ=0' 
738701     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [136] goal: 1885, source line: 206, command: 'tryclose branch' 
738792     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [137] goal: 1886, source line: 207, command: 'instantiate var=iv with='v_y_0'' 
738793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [138] goal: 1968, source line: 208, command: 'rule impLeft' 
738793     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [139] goal: 1969, source line: 209, command: 'tryclose branch' 
738798     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [140] goal: 1970, source line: 210, command: 'tryclose branch' 
738803     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [141] goal: 1789, source line: 211, command: 'tryclose branch' 
738814     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [142] goal: 1540, source line: 212, command: 'tryclose branch' 
739002     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [143] goal: 1538, source line: 213, command: 'rule getOfSwap' 
739003     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [144] goal: 2097, source line: 215, command: 'rule ifthenelse_negated' 
739004     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [145] goal: 2098, source line: 216, command: 'rule ifthenelse_split occ=0' 
739005     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [146] goal: 2099, source line: 217, command: 'tryclose branch' 
739016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [147] goal: 2100, source line: 218, command: 'tryclose branch' 
739125     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [148] goal: 1535, source line: 219, command: 'tryclose branch' 
743375     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'' 
743376     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)'' 
743382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [151] goal: 4268, source line: 226, command: 'rule andRight' 
743384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [152] goal: 4269, source line: 228, command: 'rule andRight' 
743385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [153] goal: 4271, source line: 229, command: 'rule andRight' 
743385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [154] goal: 4273, source line: 230, command: 'rule andRight' 
743386     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [155] goal: 4275, source line: 231, command: 'tryclose branch' 
743395     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [156] goal: 4276, source line: 232, command: 'rule seqNPermSwapNPerm' 
743396     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'' 
743397     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [158] goal: 4288, source line: 235, command: 'instantiate hide var=jv with='jv_0'' 
743398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [159] goal: 4289, source line: 236, command: 'rule impLeft' 
743398     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [160] goal: 4290, source line: 237, command: 'tryclose branch' 
743558     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [161] goal: 4291, source line: 238, command: 'tryclose branch' 
743563     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [162] goal: 4274, source line: 239, command: 'rule allRight' 
743564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [163] goal: 4400, source line: 241, command: 'rule impRight' 
743564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [164] goal: 4401, source line: 242, command: 'rule andLeft' 
743565     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [165] goal: 4402, source line: 243, command: 'instantiate var=iv with='v_iv_0'' 
743566     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [166] goal: 4403, source line: 244, command: 'rule impLeft' 
743567     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [167] goal: 4404, source line: 245, command: 'tryclose branch' 
743683     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [168] goal: 4405, source line: 246, command: 'rule getOfSwap' 
743685     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [169] goal: 4521, source line: 247, command: 'rule ifthenelse_negated' 
743686     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [170] goal: 4522, source line: 248, command: 'rule ifthenelse_split occ=0' 
743687     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [171] goal: 4523, source line: 249, command: 'rule andLeft' 
743688     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [172] goal: 4525, source line: 250, command: 'rule andLeft' 
743689     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [173] goal: 4526, source line: 251, command: 'rule andLeft' 
743690     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [174] goal: 4527, source line: 252, command: 'rule ifthenelse_split occ=0' 
743691     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [175] goal: 4528, source line: 253, command: 'tryclose branch' 
743795     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [176] goal: 4529, source line: 254, command: 'rule ifthenelse_split occ=0' 
743797     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [177] goal: 4622, source line: 255, command: 'tryclose branch' 
743892     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [178] goal: 4623, source line: 256, command: 'tryclose branch' 
743898     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [179] goal: 4524, source line: 257, command: 'tryclose branch' 
743904     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [180] goal: 4272, source line: 258, command: 'rule getOfSwap' 
743905     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [181] goal: 4713, source line: 260, command: 'rule ifthenelse_negated' 
743906     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [182] goal: 4714, source line: 261, command: 'rule ifthenelse_split occ=0' 
743907     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [183] goal: 4715, source line: 262, command: 'tryclose branch' 
743919     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [184] goal: 4716, source line: 263, command: 'tryclose branch' 
744014     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [185] goal: 4270, source line: 264, command: 'rule getOfSwap' 
744015     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [186] goal: 4839, source line: 266, command: 'rule ifthenelse_negated' 
744016     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [187] goal: 4840, source line: 267, command: 'rule ifthenelse_split occ=0' 
744018     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [188] goal: 4841, source line: 268, command: 'tryclose branch' 
744106     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [189] goal: 4842, source line: 269, command: 'tryclose branch' 
744118     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'' 
744119     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)'' 
744120     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [192] goal: 4950, source line: 275, command: 'rule andRight' 
744121     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [193] goal: 4951, source line: 277, command: 'rule andRight' 
744122     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [194] goal: 4953, source line: 278, command: 'rule andRight' 
744123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [195] goal: 4955, source line: 279, command: 'rule andRight' 
744123     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [196] goal: 4957, source line: 280, command: 'tryclose branch' 
744138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [197] goal: 4958, source line: 281, command: 'rule seqNPermSwapNPerm' 
744138     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [198] goal: 4977, source line: 283, command: 'instantiate hide var=iv with='jv_0'' 
744139     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'' 
744141     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [200] goal: 4979, source line: 285, command: 'rule impLeft' 
744142     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [201] goal: 4980, source line: 286, command: 'tryclose branch' 
744252     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))'' 
744253     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [203] goal: 5093, source line: 288, command: 'instantiate hide var=iv with='jv_0'' 
744254     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'' 
744255     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [205] goal: 5095, source line: 290, command: 'rule impLeft' 
744256     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [206] goal: 5096, source line: 291, command: 'tryclose branch' 
744370     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [207] goal: 5097, source line: 292, command: 'tryclose branch' 
744376     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [208] goal: 4956, source line: 293, command: 'rule allRight' 
744377     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [209] goal: 5212, source line: 295, command: 'rule impRight' 
744378     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [210] goal: 5213, source line: 296, command: 'rule andLeft' 
744379     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [211] goal: 5214, source line: 297, command: 'instantiate var=iv with='v_iv_0'' 
744380     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [212] goal: 5215, source line: 300, command: 'rule impLeft' 
744381     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [213] goal: 5216, source line: 301, command: 'tryclose branch' 
744505     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [214] goal: 5217, source line: 302, command: 'rule getOfSwap' 
744506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [215] goal: 5337, source line: 304, command: 'rule ifthenelse_negated' 
744508     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [216] goal: 5338, source line: 305, command: 'rule ifthenelse_split occ=0' 
744509     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [217] goal: 5339, source line: 306, command: 'rule andLeft' 
744510     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [218] goal: 5341, source line: 307, command: 'rule andLeft' 
744511     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [219] goal: 5342, source line: 308, command: 'rule andLeft' 
744512     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [220] goal: 5343, source line: 309, command: 'rule ifthenelse_split occ=0' 
744513     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [221] goal: 5344, source line: 310, command: 'rule getOfSwap' 
744514     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [222] goal: 5346, source line: 311, command: 'rule ifthenelse_negated' 
744515     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [223] goal: 5347, source line: 312, command: 'rule ifthenelse_split occ=0' 
744516     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [224] goal: 5348, source line: 313, command: 'rule andLeft' 
744517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [225] goal: 5350, source line: 314, command: 'rule andLeft' 
744517     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [226] goal: 5351, source line: 315, command: 'rule andLeft' 
744518     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [227] goal: 5352, source line: 316, command: 'rule ifthenelse_split occ=0' 
744519     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [228] goal: 5353, source line: 317, command: 'tryclose branch' 
744622     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [229] goal: 5354, source line: 318, command: 'rule ifthenelse_split occ=0' 
744624     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [230] goal: 5463, source line: 319, command: 'tryclose branch' 
744631     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [231] goal: 5464, source line: 320, command: 'tryclose branch' 
744726     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [232] goal: 5349, source line: 321, command: 'tryclose branch' 
744826     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [233] goal: 5345, source line: 322, command: 'rule ifthenelse_split' 
744827     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [234] goal: 5660, source line: 324, command: 'rule getOfSwap' 
744828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [235] goal: 5662, source line: 325, command: 'rule ifthenelse_negated' 
744829     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [236] goal: 5663, source line: 326, command: 'rule ifthenelse_split occ=0' 
744830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [237] goal: 5664, source line: 327, command: 'rule andLeft' 
744830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [238] goal: 5666, source line: 328, command: 'rule andLeft' 
744831     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [239] goal: 5667, source line: 329, command: 'rule andLeft' 
744832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [240] goal: 5668, source line: 330, command: 'rule ifthenelse_split occ=0' 
744832     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [241] goal: 5669, source line: 331, command: 'tryclose branch' 
744936     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [242] goal: 5670, source line: 332, command: 'tryclose branch' 
744944     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [243] goal: 5665, source line: 333, command: 'tryclose branch' 
745052     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [244] goal: 5661, source line: 334, command: 'rule getOfSwap' 
745053     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [245] goal: 5887, source line: 336, command: 'rule ifthenelse_negated' 
745054     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [246] goal: 5888, source line: 337, command: 'rule ifthenelse_split occ=0' 
745055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [247] goal: 5889, source line: 338, command: 'rule andLeft' 
745055     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [248] goal: 5891, source line: 339, command: 'rule andLeft' 
745056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [249] goal: 5892, source line: 340, command: 'rule andLeft' 
745056     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [250] goal: 5893, source line: 341, command: 'rule ifthenelse_split occ=0' 
745057     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [251] goal: 5894, source line: 342, command: 'tryclose branch' 
745064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [252] goal: 5895, source line: 343, command: 'rule ifthenelse_split occ=0' 
745064     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [253] goal: 5897, source line: 344, command: 'tryclose branch' 
745162     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [254] goal: 5898, source line: 345, command: 'tryclose branch' 
745168     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [255] goal: 5890, source line: 346, command: 'tryclose branch' 
745174     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [256] goal: 5340, source line: 347, command: 'tryclose branch' 
745295     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [257] goal: 4954, source line: 348, command: 'rule getOfSwap' 
745296     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [258] goal: 6115, source line: 350, command: 'rule ifthenelse_negated' 
745297     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [259] goal: 6116, source line: 351, command: 'rule ifthenelse_split occ=0' 
745298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [260] goal: 6117, source line: 352, command: 'rule andLeft' 
745298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [261] goal: 6119, source line: 353, command: 'rule andLeft' 
745299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [262] goal: 6120, source line: 354, command: 'rule andLeft' 
745299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [263] goal: 6121, source line: 355, command: 'rule ifthenelse_split occ=0' 
745300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [264] goal: 6122, source line: 356, command: 'tryclose branch' 
745418     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [265] goal: 6123, source line: 357, command: 'rule ifthenelse_split occ=0' 
745419     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [266] goal: 6193, source line: 358, command: 'rule getOfSwap' 
745420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [267] goal: 6195, source line: 359, command: 'rule ifthenelse_negated' 
745420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [268] goal: 6196, source line: 360, command: 'rule ifthenelse_split occ=0' 
745421     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [269] goal: 6197, source line: 361, command: 'tryclose branch' 
745427     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [270] goal: 6198, source line: 362, command: 'tryclose branch' 
745433     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [271] goal: 6194, source line: 363, command: 'tryclose branch' 
745570     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [272] goal: 6118, source line: 364, command: 'tryclose branch' 
745676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [273] goal: 4952, source line: 365, command: 'rule getOfSwap' 
745677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [274] goal: 6456, source line: 367, command: 'rule ifthenelse_negated' 
745677     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [275] goal: 6457, source line: 368, command: 'rule ifthenelse_split occ=0' 
745679     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [276] goal: 6458, source line: 369, command: 'tryclose branch' 
745880     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [277] goal: 6459, source line: 370, command: 'tryclose branch' 
745989     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'' 
745990     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [279] goal: 6735, source line: 375, command: 'tryclose branch' 
749528     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [280] goal: 6735, source line: 378, command: 'rule seqNPermSwapNPerm' 
749533     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [281] goal: 8783, source line: 380, command: 'instantiate hide var=iv with='jv_1'' 
749534     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'' 
749534     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [283] goal: 8785, source line: 382, command: 'rule impLeft' 
749535     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [284] goal: 8786, source line: 383, command: 'tryclose branch' 
749673     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))'' 
749673     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [286] goal: 8909, source line: 385, command: 'instantiate hide var=iv with='jv_1'' 
749674     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'' 
749675     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [288] goal: 8911, source line: 387, command: 'rule impLeft' 
749676     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [289] goal: 8912, source line: 388, command: 'tryclose branch' 
749802     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [290] goal: 8913, source line: 389, command: 'tryclose branch' 
753214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [291] goal: 6736, source line: 390, command: 'tryclose branch' 
756926     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [292] goal: 6736, source line: 397, command: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
756930     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'' 
756931     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [294] goal: 12634, source line: 400, command: 'instantiate hide var=jv with='jv_0'' 
756932     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [295] goal: 12635, source line: 401, command: 'rule impLeft' 
756933     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [296] goal: 12636, source line: 402, command: 'tryclose branch' 
757066     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))'' 
757066     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'' 
757068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [299] goal: 12758, source line: 405, command: 'instantiate hide var=jv with='jv_1'' 
757069     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)' ...' 
757070     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [301] goal: 12760, source line: 407, command: 'tryclose branch' 
758411     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof 
758411     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 90.8ns 
758413     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
761238     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.83s 
761238     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
762189     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: schiffl_thm_1 
762191     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8ns 
762191     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 50, command: 'macro split-prop' 
762199     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)'' 
762211     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 11, source line: 52, command: 'instantiate hide var=x with='f_x'' 
762214     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 12, source line: 53, command: 'instantiate hide var=y with='f_y'' 
762216     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [5] goal: 13, source line: 54, command: 'rule impLeft' 
762218     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [6] goal: 14, source line: 55, command: 'tryclose branch' 
762223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [7] goal: 15, source line: 56, command: 'rule exLeft' 
762223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [8] goal: 23, source line: 57, command: 'macro split-prop' 
762228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [9] goal: 27, source line: 58, command: 'rule seqPermDef occ=1' 
762228     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [10] goal: 28, source line: 59, command: 'rule andRight' 
762231     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [11] goal: 29, source line: 60, command: 'tryclose branch' 
762241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [12] goal: 30, source line: 61, command: 'instantiate hide var=s with='r_0'' 
762241     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [13] goal: 46, source line: 62, command: 'rule andRight' 
762243     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [14] goal: 47, source line: 63, command: 'tryclose branch' 
762298     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [15] goal: 48, source line: 64, command: 'rule allRight' 
762299     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [16] goal: 119, source line: 65, command: 'rule impRight' 
762300     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [17] goal: 120, source line: 66, command: 'instantiate hide var=iv with='iv_0'' 
762301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [18] goal: 121, source line: 67, command: 'rule impLeft' 
762301     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [19] goal: 122, source line: 68, command: 'tryclose branch' 
762382     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [20] goal: 123, source line: 69, command: 'rule andLeft' 
762383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [21] goal: 203, source line: 70, command: 'rule seqNPermRange' 
762383     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [22] goal: 204, source line: 71, command: 'instantiate hide var=iv with='iv_0'' 
762384     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [23] goal: 205, source line: 72, command: 'rule impLeft' 
762385     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [24] goal: 206, source line: 73, command: 'tryclose branch' 
762390     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [25] goal: 207, source line: 74, command: 'rule andLeft' 
762391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [26] goal: 215, source line: 75, command: 'rule andLeft' 
762391     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [27] goal: 216, source line: 76, command: 'rule seqNPermRange' 
762392     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [28] goal: 217, source line: 77, command: 'instantiate hide var=iv with='f_x'' 
762393     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [29] goal: 218, source line: 78, command: 'rule impLeft' 
762394     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [30] goal: 219, source line: 79, command: 'tryclose branch' 
762499     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [31] goal: 220, source line: 80, command: 'rule andLeft' 
762500     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [32] goal: 311, source line: 81, command: 'rule andLeft' 
762501     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [33] goal: 312, source line: 82, command: 'rule seqNPermRange' 
762502     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [34] goal: 313, source line: 83, command: 'instantiate hide var=iv with='f_y'' 
762503     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [35] goal: 314, source line: 84, command: 'rule impLeft' 
762504     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [36] goal: 315, source line: 85, command: 'tryclose branch' 
762603     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [37] goal: 316, source line: 86, command: 'rule andLeft' 
762604     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [38] goal: 410, source line: 87, command: 'rule andLeft' 
762605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [39] goal: 411, source line: 88, command: 'rule getOfSeqDef occ=0' 
762605     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [40] goal: 412, source line: 89, command: 'rule getOfSeqDef' 
762606     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [41] goal: 413, source line: 90, command: 'rule ifthenelse_split occ=0' 
762607     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [42] goal: 414, source line: 91, command: 'rule andLeft occ=0' 
762608     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [43] goal: 416, source line: 92, command: 'rule sub_zero_2 occ=0' 
762609     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [44] goal: 417, source line: 93, command: 'rule ifthenelse_split occ=2' 
762610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [45] goal: 418, source line: 94, command: 'rule andLeft' 
762610     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [46] goal: 420, source line: 95, command: 'rule sub_zero_2 occ=0' 
762611     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [47] goal: 421, source line: 96, command: 'rule add_zero_right occ=0' 
762612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [48] goal: 422, source line: 97, command: 'rule add_zero_right occ=0' 
762612     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [49] goal: 423, source line: 98, command: 'rule add_zero_right occ=0' 
762613     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [50] goal: 424, source line: 99, command: 'rule add_zero_right occ=0' 
762614     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [51] goal: 425, source line: 100, command: 'rule add_zero_right occ=0' 
762615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [52] goal: 426, source line: 101, command: 'rule add_zero_right occ=0' 
762615     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [53] goal: 427, source line: 102, command: 'rule ifthenelse_split occ=0' 
762616     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [54] goal: 428, source line: 103, command: 'rule ifthenelse_split occ=0' 
762617     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [55] goal: 430, source line: 104, command: 'tryclose branch' 
762620     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [56] goal: 431, source line: 105, command: 'tryclose branch' 
762661     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [57] goal: 429, source line: 106, command: 'rule ifthenelse_split occ=0' 
762662     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [58] goal: 473, source line: 107, command: 'tryclose branch' 
762718     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [59] goal: 474, source line: 108, command: 'rule ifthenelse_split occ=0' 
762720     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [60] goal: 541, source line: 109, command: 'rule seqNPermInjective' 
762721     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [61] goal: 543, source line: 110, command: 'instantiate hide var=iv with='iv_0'' 
762722     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [62] goal: 544, source line: 111, command: 'instantiate hide var=jv with='f_y'' 
762723     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [63] goal: 545, source line: 112, command: 'rule impLeft' 
762724     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [64] goal: 546, source line: 113, command: 'tryclose branch' 
762772     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [65] goal: 547, source line: 114, command: 'tryclose branch' 
762774     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [66] goal: 542, source line: 115, command: 'rule ifthenelse_split occ=0' 
762775     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [67] goal: 606, source line: 116, command: 'rule seqNPermInjective' 
762776     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [68] goal: 608, source line: 117, command: 'instantiate hide var=iv with='iv_0'' 
762777     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [69] goal: 609, source line: 118, command: 'instantiate hide var=jv with='f_x'' 
762778     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [70] goal: 610, source line: 119, command: 'rule impLeft' 
762779     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [71] goal: 611, source line: 120, command: 'tryclose branch' 
762828     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [72] goal: 612, source line: 121, command: 'tryclose branch' 
762830     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [73] goal: 607, source line: 122, command: 'tryclose branch' 
762834     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [74] goal: 419, source line: 123, command: 'tryclose branch' 
762895     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [75] goal: 415, source line: 124, command: 'tryclose branch' 
762958     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from tacletProofs/seqRules/Taclet_eqSameSeq.proof 
762958     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 86.2ns 
762959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
765842     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 2.88s 
765842     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq 
766865     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof Taclet: eqSameSeq 
766885     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 16.82ms