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

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

tests
0

failures
0

ignored
14m50.02s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.277s passed
powPositiveConcrete data()[101] 4.378s passed
powGeq1Concrete data()[102] 4.407s passed
pow2InIntLower data()[103] 4.486s passed
pow2InIntUpper data()[104] 4.529s passed
logSelfConcrete data()[105] 4.441s passed
log1Concrete data()[106] 4.299s passed
logProduct data()[107] 4.383s passed
logTimesBaseConcrete data()[108] 4.467s passed
logProdIdentity data()[109] 4.412s passed
moduloByteIsInByte data()[10] 4.667s passed
logProdIdentityConcrete data()[110] 4.300s passed
logPowIdentity data()[111] 4.354s passed
logPowIdentityConcrete data()[112] 4.420s passed
logPositive data()[113] 4.375s passed
logPositiveConcrete data()[114] 4.330s passed
logMono data()[115] 4.411s passed
logMonoConcrete data()[116] 4.288s passed
powLogLess data()[117] 4.350s passed
powLogMore2 data()[118] 4.423s passed
logLessThanPow data()[119] 4.430s passed
moduloCharIsInChar data()[11] 4.431s passed
logLessThanPowConcrete data()[120] 4.430s passed
logSqueeze data()[121] 4.400s passed
ifthenelse_equals data()[122] 4.431s passed
ifthenelse_equals_1 data()[123] 4.353s passed
ifthenelse_equals_2 data()[124] 4.330s passed
disjointWithSingleton1 data()[125] 4.455s passed
disjointWithSingleton2 data()[126] 4.400s passed
disjointArrayRanges data()[127] 4.420s passed
disjointArrayRangeAllFields1 data()[128] 4.483s passed
disjointArrayRangeAllFields2 data()[129] 4.358s passed
div_unique1 data()[12] 4.543s passed
seqSelfDefinition data()[130] 4.426s passed
seqOutsideValue data()[131] 4.400s passed
castedGetAny data()[132] 4.378s passed
seqGetAlphaCast data()[133] 4.544s passed
getOfSeqSingleton data()[134] 4.605s passed
getOfSeqSingletonConcrete data()[135] 4.517s passed
getOfSeqConcat data()[136] 4.476s passed
getOfSeqSub data()[137] 4.396s passed
getOfSeqReverse data()[138] 4.392s passed
lenOfSeqEmpty data()[139] 4.453s passed
div_unique2 data()[13] 4.445s passed
lenOfSeqSingleton data()[140] 4.382s passed
lenOfSeqConcat data()[141] 4.500s passed
lenOfSeqSub data()[142] 4.418s passed
lenOfSeqReverse data()[143] 4.336s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.319s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.367s passed
getOfSeqSingletonEQ data()[146] 4.449s passed
getOfSeqConcatEQ data()[147] 4.304s passed
getOfSeqSubEQ data()[148] 4.241s passed
getOfSeqReverseEQ data()[149] 4.339s passed
div_exists data()[14] 4.727s passed
lenOfSeqEmptyEQ data()[150] 4.297s passed
lenOfSeqSingletonEQ data()[151] 4.276s passed
lenOfSeqConcatEQ data()[152] 4.279s passed
lenOfSeqSubEQ data()[153] 4.321s passed
lenOfSeqReverseEQ data()[154] 4.311s passed
getOfSeqDefEQ data()[155] 4.398s passed
lenOfSeqDefEQ data()[156] 4.371s passed
seqConcatWithSeqEmpty1 data()[157] 4.361s passed
seqConcatWithSeqEmpty2 data()[158] 4.345s passed
seqReverseOfSeqEmpty data()[159] 4.331s passed
div_one data()[15] 4.473s passed
subSeqComplete data()[160] 4.352s passed
subSeqTailR data()[161] 4.331s passed
subSeqTailL data()[162] 4.340s passed
subSeqTailEQR data()[163] 4.321s passed
subSeqTailEQL data()[164] 4.323s passed
seqDef_split data()[165] 4.448s passed
seqDef_induction_upper data()[166] 4.455s passed
seqDef_induction_upper_concrete data()[167] 4.413s passed
seqDef_induction_lower data()[168] 4.396s passed
seqDef_induction_lower_concrete data()[169] 4.391s passed
jdiv_one data()[16] 4.577s passed
seqDef_split_in_three data()[170] 4.634s passed
seqDef_empty data()[171] 4.356s passed
seqDef_one_summand data()[172] 4.306s passed
seqDef_lower_equals_upper data()[173] 4.345s passed
seqDefOfSeq data()[174] 4.354s passed
seqSelfDefinitionEQ2 data()[175] 4.274s passed
indexOfSeqSingleton data()[176] 4.337s passed
indexOfSeqConcatFirst data()[177] 4.325s passed
indexOfSeqConcatSecond data()[178] 4.374s passed
indexOfSeqSub data()[179] 4.421s passed
div_zero data()[17] 4.486s passed
lenOfArray2seq data()[180] 4.336s passed
getAnyOfArray2seq data()[181] 4.347s passed
getOfArray2seq data()[182] 4.264s passed
getAnyOfNPermInv data()[183] 4.328s passed
seqNPermRange data()[184] 4.468s passed
seqPermTrans data()[185] 4.588s passed
seqPermRefl data()[186] 4.357s passed
seqPermSplit data()[187] 4.272s passed
seqNPermRight data()[188] 4.903s passed
seqPermFromSwap data()[189] 4.532s passed
divResZero1 data()[18] 4.465s passed
seqPermTransAlt0 data()[190] 4.351s passed
seqPermTransAlt1 data()[191] 4.382s passed
seqPermTransAlt2 data()[192] 4.384s passed
seqPermTransAlt3 data()[193] 4.405s passed
schiffl_lemma_2 data()[194] 29.062s passed
schiffl_thm_1 data()[195] 5.266s passed
eqSameSeq data()[196] 4.862s passed
divResZero2 data()[19] 4.546s passed
eqTermCut data()[1] 5.587s passed
divResOne1 data()[20] 4.498s passed
divResOne2 data()[21] 4.484s passed
div_cancel1 data()[22] 4.587s passed
div_cancel2 data()[23] 4.427s passed
divAddMultDenom data()[24] 4.493s passed
divMinus data()[25] 4.554s passed
divMinusDenom data()[26] 4.632s passed
divLeastDPos data()[27] 4.383s passed
divLeastDNeg data()[28] 4.339s passed
divGreatestDPos data()[29] 4.279s passed
equivAllRight data()[2] 5.061s passed
divGreatestDNeg data()[30] 4.339s passed
divIncreasingPos data()[31] 4.413s passed
divIncreasingNeg data()[32] 4.293s passed
jdiv_zero data()[33] 4.330s passed
jdivPulloutMinusNum data()[34] 4.480s passed
jdivPulloutMinusDenom data()[35] 4.361s passed
jdiv_uniquePosPos data()[36] 4.265s passed
jdiv_uniquePosNeg data()[37] 4.309s passed
jdiv_uniqueNegPos data()[38] 4.298s passed
jdiv_uniqueNegNeg data()[39] 4.169s passed
irrflConcrete1 data()[3] 4.904s passed
jdivMultDenom1 data()[40] 4.201s passed
jdivMultDenom2 data()[41] 4.057s passed
mod_geZero data()[42] 3.955s passed
mod_lessDenom data()[43] 3.932s passed
jmod_NumPos data()[44] 4.054s passed
jmod_NumNeg data()[45] 4.219s passed
jmod_geZero data()[46] 4.312s passed
jmodNumZero data()[47] 4.286s passed
jmod_pulloutminusNum data()[48] 4.378s passed
jmod_pulloutminusDenom data()[49] 4.338s passed
irrflConcrete2 data()[4] 4.703s passed
jmodUnique1 data()[50] 4.510s passed
jmodUnique2 data()[51] 4.665s passed
intDivRem data()[52] 4.283s passed
jmodjmod data()[53] 4.327s passed
jmodDivisible data()[54] 4.343s passed
jmodDivisibleRep data()[55] 4.250s passed
jdivAddMultDenom data()[56] 4.864s passed
jmodAltZero data()[57] 4.343s passed
jmodAddMultDenomZero data()[58] 4.388s passed
polyDiv_zero data()[59] 4.377s passed
cancel_gtPos data()[5] 4.763s passed
polyMod_ltdivDenom data()[60] 4.396s passed
bsum_empty data()[61] 4.352s passed
bsum_induction_upper data()[62] 4.408s passed
bsum_induction_lower data()[63] 4.441s passed
bsum_num_of_bounds data()[64] 4.375s passed
bsum_num_of_bounds2 data()[65] 4.366s passed
bsum_induction_upper2 data()[66] 4.188s passed
bsum_induction_upper_concrete data()[67] 4.336s passed
bsum_induction_upper_concrete_2 data()[68] 4.442s passed
bsum_induction_upper2_concrete data()[69] 4.352s passed
cancel_gtNeg data()[6] 4.600s passed
bsum_induction_lower_concrete data()[70] 4.625s passed
bsum_induction_lower2 data()[71] 4.313s passed
bsum_induction_lower2_concrete data()[72] 4.353s passed
bsum_positive data()[73] 4.476s passed
bsum_upper_bound data()[74] 4.338s passed
bsum_lower_bound data()[75] 4.370s passed
bsum_positive_lower_bound_element data()[76] 4.412s passed
bsum_sub_same_index data()[77] 4.488s passed
bsum_less_same_index data()[78] 4.515s passed
bsum_equal_except_one_index data()[79] 4.322s passed
moduloIntIsInInt data()[7] 4.582s passed
bsum_num_of_is_max data()[80] 4.363s passed
bsum_num_of_is_max2 data()[81] 4.383s passed
bsum_num_of_is_max3 data()[82] 4.343s passed
bsum_num_of_is_max4 data()[83] 4.556s passed
bsum_num_of_lt_max data()[84] 4.591s passed
bsum_num_of_lt_max2 data()[85] 4.561s passed
bsum_num_of_lt_max3 data()[86] 4.461s passed
bsum_num_of_lt_max4 data()[87] 4.443s passed
bsum_num_of_gt0 data()[88] 4.357s passed
bsum_num_of_gt0_alt data()[89] 4.357s passed
moduloLongIsInLong data()[8] 4.511s passed
bsum_add_concrete data()[90] 4.341s passed
bprod_all_positive data()[91] 4.330s passed
bprod_split data()[92] 4.393s passed
powConcrete0 data()[93] 4.371s passed
powConcrete1 data()[94] 4.356s passed
powSplitFactor data()[95] 4.298s passed
powAdd data()[96] 4.346s passed
powMono data()[97] 4.288s passed
powMonoConcrete data()[98] 4.296s passed
powMonoConcreteRight data()[99] 4.178s passed
moduloShortIsInShort data()[9] 4.500s passed

Standard output

1035       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)

16482      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqTermCut 
21817      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equivAllRight 
26684      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete1 
31524      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: irrflConcrete2 
36158      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtPos 
40855      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: cancel_gtNeg 
45472      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloIntIsInInt 
49991      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloLongIsInLong 
54505      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloShortIsInShort 
59178      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloByteIsInByte 
63666      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: moduloCharIsInChar 
68111      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique1 
72552      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_unique2 
77036      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_exists 
81832      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_one 
86373      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_one 
90788      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_zero 
95359      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero1 
99848      INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResZero2 
104370     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne1 
108813     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divResOne2 
113433     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel1 
117900     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: div_cancel2 
122285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divAddMultDenom 
126794     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinus 
131512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divMinusDenom 
135982     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDPos 
140309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divLeastDNeg 
144592     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDPos 
148940     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divGreatestDNeg 
153304     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingPos 
157654     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: divIncreasingNeg 
161954     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_zero 
166389     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusNum 
170734     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivPulloutMinusDenom 
175102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosPos 
179386     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniquePosNeg 
183690     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegPos 
187872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdiv_uniqueNegNeg 
192020     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom1 
196207     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivMultDenom2 
200165     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_geZero 
204103     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: mod_lessDenom 
208171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumPos 
212377     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_NumNeg 
216611     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_geZero 
220939     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodNumZero 
225246     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusNum 
229628     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmod_pulloutminusDenom 
233865     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique1 
238477     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodUnique2 
243073     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: intDivRem 
247320     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodjmod 
251720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisible 
255979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodDivisibleRep 
260360     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jdivAddMultDenom 
265202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAltZero 
269573     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: jmodAddMultDenomZero 
273911     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyDiv_zero 
278332     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: polyMod_ltdivDenom 
282720     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_empty 
287110     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper 
291512     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower 
295885     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds 
300288     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_bounds2 
304521     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2 
308781     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete 
313266     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper_concrete_2 
317588     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_upper2_concrete 
322184     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower_concrete 
326563     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2 
330922     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_induction_lower2_concrete 
335339     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive 
339707     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_upper_bound 
344035     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_lower_bound 
348429     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_positive_lower_bound_element 
352960     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_sub_same_index 
357420     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_less_same_index 
361772     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_equal_except_one_index 
366163     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max 
370556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max2 
374920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max3 
379407     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_is_max4 
383957     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max 
388530     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max2 
393009     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max3 
397458     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_lt_max4 
401879     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0 
406236     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_num_of_gt0_alt 
410612     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bsum_add_concrete 
414907     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_all_positive 
419256     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: bprod_split 
423679     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete0 
428067     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powConcrete1 
432342     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powSplitFactor 
436714     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powAdd 
440992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMono 
445301     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcrete 
449502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powMonoConcreteRight 
453738     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositive 
458124     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powPositiveConcrete 
462496     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powGeq1Concrete 
466920     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntLower 
471510     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: pow2InIntUpper 
475948     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSelfConcrete 
480306     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: log1Concrete 
484655     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProduct 
489113     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logTimesBaseConcrete 
493502     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentity 
497868     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logProdIdentityConcrete 
502186     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentity 
506590     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPowIdentityConcrete 
510969     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositive 
515309     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logPositiveConcrete 
519632     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMono 
524026     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logMonoConcrete 
528329     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogLess 
532740     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: powLogMore2 
537150     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPow 
541659     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logLessThanPowConcrete 
546029     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: logSqueeze 
550472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals 
554826     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_1 
559153     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: ifthenelse_equals_2 
563616     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton1 
568024     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointWithSingleton2 
572403     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRanges 
576872     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields1 
581224     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: disjointArrayRangeAllFields2 
585674     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinition 
590078     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqOutsideValue 
594479     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: castedGetAny 
598979     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqGetAlphaCast 
603580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingleton 
608148     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonConcrete 
612580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcat 
617016     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSub 
621394     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverse 
625890     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmpty 
630225     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingleton 
634717     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcat 
639139     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSub 
643517     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverse 
647819     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenLeft 
652192     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: equalityToSeqGetAndSeqLenRight 
656556     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSingletonEQ 
660930     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqConcatEQ 
665202     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqSubEQ 
669535     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqReverseEQ 
673844     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqEmptyEQ 
678102     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSingletonEQ 
682365     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqConcatEQ 
686709     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqSubEQ 
691018     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqReverseEQ 
695400     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfSeqDefEQ 
699752     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfSeqDefEQ 
704099     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty1 
708472     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqConcatWithSeqEmpty2 
712787     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqReverseOfSeqEmpty 
717171     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqComplete 
721485     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailR 
725805     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailL 
730144     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQR 
734447     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: subSeqTailEQL 
738810     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split 
743305     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper 
747739     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_upper_concrete 
752134     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower 
756494     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_induction_lower_concrete 
760870     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_split_in_three 
765568     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_empty 
769871     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_one_summand 
774203     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDef_lower_equals_upper 
778538     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqDefOfSeq 
782864     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqSelfDefinitionEQ2 
787198     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSingleton 
791481     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatFirst 
795828     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqConcatSecond 
800285     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: indexOfSeqSub 
804643     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: lenOfArray2seq 
808978     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfArray2seq 
813258     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getOfArray2seq 
817580     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: getAnyOfNPermInv 
821906     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRange 
826464     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTrans 
830992     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermRefl 
835282     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermSplit 
839595     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqNPermRight 
844486     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermFromSwap 
849045     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt0 
853423     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt1 
857833     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt2 
862177     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: seqPermTransAlt3 
866586     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_lemma_2 
867724     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
867791     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight' 
867821     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight' 
867827     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'macro split-prop' 
867835     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule 'seqPermDefLeft'' 
867839     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'rule 'andLeft'' 
867841     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule 'exLeft'' 
867846     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
867853     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule  seqNPermRange' 
867855     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'instantiate var=iv with='v_x_0' occ=1' 
867864     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'rule impLeft' 
867866     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'tryclose branch' 
868177     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andLeft' 
868178     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'rule andLeft' 
868180     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'instantiate var=iv with='v_y_0' occ=1' 
868181     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impLeft' 
868182     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'tryclose branch' 
868336     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule andLeft' 
868338     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'rule andLeft' 
868339     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule seqNPermDefLeft' 
868341     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'instantiate var=iv with='v_x_0' occ=2' 
868343     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'rule impLeft' 
868344     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'tryclose branch' 
868572     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'rule exLeft' 
868576     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
868577     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
868579     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'instantiate hide var=iv with='v_y_0' occ=2' 
868580     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'rule impLeft' 
868582     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'tryclose branch' 
868739     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'rule exLeft' 
868742     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
868743     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
868744     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'instantiate var=iv with='jv_0' occ=1' 
868746     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'rule impLeft' 
868747     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'tryclose branch' 
868755     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'rule andLeft' 
868757     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
868758     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule castAdd formula='s_0[jv_0] = v_x_0' occ=0' 
868761     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'instantiate hide var=iv with='jv_1' occ=1' 
868765     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule impLeft' 
868767     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'tryclose branch' 
868777     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft' 
868779     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule andLeft' 
868781     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule castAdd formula='s_0[jv_1] = v_y_0' occ=0' 
868782     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'instantiate var=iv  with='v_x_0'' 
868783     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule impLeft' 
868784     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'tryclose branch' 
868956     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'instantiate var=iv  with='v_y_0'' 
868957     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule impLeft' 
868959     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'tryclose branch' 
869103     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'cut 'v_x_0 = v_y_0'' 
869105     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'instantiate hide var='v_r' with='seqSwap(s_0,v_x_0,jv_0)'' 
869108     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule andRight' 
869110     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule andRight' 
869112     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'rule andRight' 
869113     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'rule andRight' 
869115     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule lenOfSwap' 
869116     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
869123     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule seqNPermSwapNPerm' 
869128     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'instantiate hide var='iv' with='v_x_0' occ=1' 
869129     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var='jv' with='jv_0'' 
869130     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'rule impLeft' 
869132     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'tryclose branch' 
869299     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
869303     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'rule allRight' 
869307     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule impRight' 
869309     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule andLeft' 
869310     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate var=iv with='v_iv_0'' 
869312     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'rule impLeft' 
869313     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'tryclose branch' 
869454     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'rule getOfSwap' 
869456     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'rule ifthenelse_negated' 
869457     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'rule ifthenelse_split occ=0' 
869459     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'rule andLeft' 
869460     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'rule andLeft' 
869462     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 76: 'rule andLeft' 
869463     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 77: 'rule ifthenelse_split occ=0' 
869465     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 78: 'tryclose branch' 
869592     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 79: 'rule ifthenelse_split occ=0' 
869594     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 80: 'tryclose branch' 
869719     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 81: 'tryclose branch' 
869725     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 82: 'tryclose branch' 
869731     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 83: 'rule getOfSwap' 
869733     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 84: 'rule ifthenelse_negated' 
869735     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 85: 'rule ifthenelse_split occ=0' 
869737     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 86: 'rule andLeft' 
869738     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 87: 'rule andLeft' 
869740     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 88: 'rule andLeft' 
869740     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 89: 'rule ifthenelse_split occ=0' 
869745     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 90: 'tryclose branch' 
869756     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 91: 'tryclose branch' 
869761     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 92: 'tryclose branch' 
869867     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 93: 'rule getOfSwap' 
869869     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 94: 'rule ifthenelse_negated' 
869870     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 95: 'rule ifthenelse_split occ=0' 
869872     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 96: 'rule andLeft' 
869873     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 97: 'rule andLeft' 
869873     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 98: 'rule andLeft' 
869874     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 99: 'rule ifthenelse_split occ=0' 
869875     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 100: 'tryclose branch' 
869954     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 101: 'tryclose branch' 
869960     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 102: 'tryclose branch' 
870072     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 103: 'cut '(int)s_0[v_x_0] = (int)s_0[v_y_0]'' 
870074     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 104: 'rule seqNPermInjective' 
870077     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 105: 'instantiate hide var=iv with='v_x_0'' 
870079     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 106: 'instantiate hide var=jv with='v_y_0'' 
870080     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 107: 'rule impLeft' 
870081     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 108: 'tryclose branch' 
870246     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 109: 'tryclose branch' 
870251     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 110: 'cut '(int)s_0[v_x_0] = v_x_0'' 
870253     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 111: 'instantiate hide var=v_r with='seqSwap(s_0,v_y_0,jv_1)'' 
870255     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 112: 'rule andRight' 
870257     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 113: 'rule andRight' 
870258     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 114: 'rule andRight' 
870259     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 115: 'rule andRight' 
870260     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 116: 'tryclose branch' 
870272     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 117: 'rule seqNPermSwapNPerm' 
870276     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 118: 'instantiate hide var=iv with='v_y_0'' 
870277     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 119: 'instantiate hide var=jv with='jv_1'' 
870278     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 120: 'tryclose branch' 
870411     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 121: 'rule allRight' 
870413     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 122: 'rule impRight' 
870414     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 123: 'rule andLeft' 
870415     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 124: 'instantiate var=iv with='v_iv_0'' 
870416     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 125: 'rule impLeft' 
870417     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 126: 'tryclose branch' 
870547     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 127: 'rule getOfSwap' 
870549     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 128: 'rule ifthenelse_negated' 
870550     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 129: 'rule ifthenelse_split occ=0' 
870552     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 130: 'rule andLeft' 
870553     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 131: 'rule andLeft' 
870554     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 132: 'rule andLeft' 
870554     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 133: 'rule ifthenelse_split occ=0' 
870556     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 134: 'tryclose branch' 
870661     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 135: 'rule ifthenelse_split occ=0' 
870663     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 136: 'tryclose branch' 
870758     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 137: 'instantiate var=iv with='v_y_0'' 
870758     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 138: 'rule impLeft' 
870759     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 139: 'tryclose branch' 
870765     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 140: 'tryclose branch' 
870769     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 141: 'tryclose branch' 
870774     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 142: 'tryclose branch' 
870980     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 143: 'rule getOfSwap' 
870981     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 144: 'rule ifthenelse_negated' 
870982     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 145: 'rule ifthenelse_split occ=0' 
870983     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 146: 'tryclose branch' 
870995     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 147: 'tryclose branch' 
871117     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 148: 'tryclose branch' 
875657     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 149: 'cut  '(int)s_0[v_y_0] = v_y_0'' 
875658     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 150: 'instantiate hide var=v_r with='seqSwap(s_0,v_x_0,jv_0)'' 
875665     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 151: 'rule andRight' 
875666     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 152: 'rule andRight' 
875668     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 153: 'rule andRight' 
875669     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 154: 'rule andRight' 
875671     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 155: 'tryclose branch' 
875684     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 156: 'rule seqNPermSwapNPerm' 
875686     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 157: 'instantiate hide var=iv with='v_x_0'' 
875688     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 158: 'instantiate hide var=jv with='jv_0'' 
875689     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 159: 'rule impLeft' 
875689     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 160: 'tryclose branch' 
875817     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 161: 'tryclose branch' 
875822     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 162: 'rule allRight' 
875824     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 163: 'rule impRight' 
875825     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 164: 'rule andLeft' 
875826     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 165: 'instantiate var=iv with='v_iv_0'' 
875827     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 166: 'rule impLeft' 
875828     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 167: 'tryclose branch' 
875963     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 168: 'rule getOfSwap' 
875965     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 169: 'rule ifthenelse_negated' 
875966     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 170: 'rule ifthenelse_split occ=0' 
875967     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 171: 'rule andLeft' 
875968     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 172: 'rule andLeft' 
875968     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 173: 'rule andLeft' 
875969     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 174: 'rule ifthenelse_split occ=0' 
875970     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 175: 'tryclose branch' 
876070     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 176: 'rule ifthenelse_split occ=0' 
876072     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 177: 'tryclose branch' 
876165     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 178: 'tryclose branch' 
876170     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 179: 'tryclose branch' 
876176     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 180: 'rule getOfSwap' 
876177     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 181: 'rule ifthenelse_negated' 
876178     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 182: 'rule ifthenelse_split occ=0' 
876179     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 183: 'tryclose branch' 
876192     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 184: 'tryclose branch' 
876293     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 185: 'rule getOfSwap' 
876294     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 186: 'rule ifthenelse_negated' 
876295     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 187: 'rule ifthenelse_split occ=0' 
876296     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 188: 'tryclose branch' 
876391     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 189: 'tryclose branch' 
876406     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 190: 'cut '(int)s_0[v_x_0]=v_y_0'' 
876407     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 191: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0,jv_0,v_x_0),jv_0,v_y_0)'' 
876409     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 192: 'rule andRight' 
876410     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 193: 'rule andRight' 
876411     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 194: 'rule andRight' 
876411     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 195: 'rule andRight' 
876412     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 196: 'tryclose branch' 
876426     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 197: 'rule seqNPermSwapNPerm' 
876427     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 198: 'instantiate hide var=iv with='jv_0'' 
876429     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 199: 'instantiate hide var=jv with='v_x_0'' 
876429     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 200: 'rule impLeft' 
876430     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 201: 'tryclose branch' 
876547     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 202: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0, jv_0, v_x_0))'' 
876549     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 203: 'instantiate hide var=iv with='jv_0'' 
876551     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 204: 'instantiate hide var=jv with='v_y_0'' 
876551     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 205: 'rule impLeft' 
876552     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 206: 'tryclose branch' 
876674     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 207: 'tryclose branch' 
876681     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 208: 'rule allRight' 
876682     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 209: 'rule impRight' 
876683     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 210: 'rule andLeft' 
876683     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 211: 'instantiate var=iv with='v_iv_0'' 
876684     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 212: 'rule impLeft' 
876685     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 213: 'tryclose branch' 
876811     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 214: 'rule getOfSwap' 
876813     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 215: 'rule ifthenelse_negated' 
876813     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 216: 'rule ifthenelse_split occ=0' 
876815     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 217: 'rule andLeft' 
876815     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 218: 'rule andLeft' 
876816     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 219: 'rule andLeft' 
876817     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 220: 'rule ifthenelse_split occ=0' 
876818     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 221: 'rule getOfSwap' 
876819     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 222: 'rule ifthenelse_negated' 
876820     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 223: 'rule ifthenelse_split occ=0' 
876822     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 224: 'rule andLeft' 
876822     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 225: 'rule andLeft' 
876823     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 226: 'rule andLeft' 
876823     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 227: 'rule ifthenelse_split occ=0' 
876824     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 228: 'tryclose branch' 
876939     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 229: 'rule ifthenelse_split occ=0' 
876941     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 230: 'tryclose branch' 
876948     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 231: 'tryclose branch' 
877048     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 232: 'tryclose branch' 
877151     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 233: 'rule ifthenelse_split' 
877153     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 234: 'rule getOfSwap' 
877154     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 235: 'rule ifthenelse_negated' 
877155     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 236: 'rule ifthenelse_split occ=0' 
877156     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 237: 'rule andLeft' 
877156     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 238: 'rule andLeft' 
877156     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 239: 'rule andLeft' 
877157     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 240: 'rule ifthenelse_split occ=0' 
877159     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 241: 'tryclose branch' 
877271     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 242: 'tryclose branch' 
877280     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 243: 'tryclose branch' 
877395     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 244: 'rule getOfSwap' 
877397     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 245: 'rule ifthenelse_negated' 
877398     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 246: 'rule ifthenelse_split occ=0' 
877399     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 247: 'rule andLeft' 
877399     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 248: 'rule andLeft' 
877400     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 249: 'rule andLeft' 
877400     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 250: 'rule ifthenelse_split occ=0' 
877401     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 251: 'tryclose branch' 
877408     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 252: 'rule ifthenelse_split occ=0' 
877409     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 253: 'tryclose branch' 
877511     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 254: 'tryclose branch' 
877518     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 255: 'tryclose branch' 
877524     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 256: 'tryclose branch' 
877704     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 257: 'rule getOfSwap' 
877705     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 258: 'rule ifthenelse_negated' 
877706     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 259: 'rule ifthenelse_split occ=0' 
877707     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 260: 'rule andLeft' 
877708     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 261: 'rule andLeft' 
877708     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 262: 'rule andLeft' 
877709     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 263: 'rule ifthenelse_split occ=0' 
877710     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 264: 'tryclose branch' 
877783     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 265: 'rule ifthenelse_split occ=0' 
877789     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 266: 'rule getOfSwap' 
877790     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 267: 'rule ifthenelse_negated' 
877791     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 268: 'rule ifthenelse_split occ=0' 
877792     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 269: 'tryclose branch' 
877798     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 270: 'tryclose branch' 
877804     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 271: 'tryclose branch' 
877956     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 272: 'tryclose branch' 
878069     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 273: 'rule getOfSwap' 
878070     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 274: 'rule ifthenelse_negated' 
878071     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 275: 'rule ifthenelse_split occ=0' 
878073     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 276: 'tryclose branch' 
878284     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 277: 'tryclose branch' 
878397     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 278: 'cut 'int::seqGet(s_0, v_y_0)=v_x_0'' 
878398     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 279: 'tryclose branch' 
882343     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 280: 'rule seqNPermSwapNPerm' 
882350     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 281: 'instantiate hide var=iv with='jv_1'' 
882352     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 282: 'instantiate hide var=jv with='v_y_0'' 
882352     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 283: 'rule impLeft' 
882353     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 284: 'tryclose branch' 
882500     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 285: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,jv_1,v_y_0))'' 
882502     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 286: 'instantiate hide var=iv with='jv_1'' 
882503     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 287: 'instantiate hide var=jv with='v_x_0'' 
882504     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 288: 'rule impLeft' 
882505     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 289: 'tryclose branch' 
882644     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 290: 'tryclose branch' 
886641     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 291: 'tryclose branch' 
890680     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 292: 'rule seqNPermSwapNPerm formula='seqNPerm(s_0)'' 
890686     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 293: 'instantiate hide var=iv with='v_x_0'' 
890689     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 294: 'instantiate hide var=jv with='jv_0'' 
890690     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 295: 'rule impLeft' 
890691     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 296: 'tryclose branch' 
890840     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 297: 'rule seqNPermSwapNPerm formula='seqNPerm(seqSwap(s_0,v_x_0,jv_0))'' 
890842     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 298: 'instantiate hide var=iv with='v_y_0'' 
890844     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 299: 'instantiate hide var=jv with='jv_1'' 
890845     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 300: 'instantiate hide var=v_r with='seqSwap(seqSwap(s_0, v_x_0, jv_0), v_y_0, jv_1)' ...' 
890847     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 301: 'tryclose branch' 
895754     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: schiffl_thm_1 
896863     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' 
896874     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule schiffl_lemma_2 formula='seqPerm(f_s, f_t)'' 
896889     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'instantiate hide var=x with='f_x'' 
896892     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 4: 'instantiate hide var=y with='f_y'' 
896895     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 5: 'rule impLeft' 
896895     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 6: 'tryclose branch' 
896901     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 7: 'rule exLeft' 
896903     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 8: 'macro split-prop' 
896908     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 9: 'rule seqPermDef occ=1' 
896911     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 10: 'rule andRight' 
896912     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 11: 'tryclose branch' 
896923     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 12: 'instantiate hide var=s with='r_0'' 
896926     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 13: 'rule andRight' 
896927     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 14: 'tryclose branch' 
896984     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 15: 'rule allRight' 
896985     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 16: 'rule impRight' 
896986     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 17: 'instantiate hide var=iv with='iv_0'' 
896986     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 18: 'rule impLeft' 
896987     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 19: 'tryclose branch' 
897061     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 20: 'rule andLeft' 
897061     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 21: 'rule seqNPermRange' 
897063     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 22: 'instantiate hide var=iv with='iv_0'' 
897064     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 23: 'rule impLeft' 
897065     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 24: 'tryclose branch' 
897068     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 25: 'rule andLeft' 
897069     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 26: 'rule andLeft' 
897069     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 27: 'rule seqNPermRange' 
897070     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 28: 'instantiate hide var=iv with='f_x'' 
897071     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 29: 'rule impLeft' 
897072     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 30: 'tryclose branch' 
897161     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 31: 'rule andLeft' 
897162     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 32: 'rule andLeft' 
897163     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 33: 'rule seqNPermRange' 
897165     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 34: 'instantiate hide var=iv with='f_y'' 
897166     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 35: 'rule impLeft' 
897166     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 36: 'tryclose branch' 
897251     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 37: 'rule andLeft' 
897252     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 38: 'rule andLeft' 
897253     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 39: 'rule getOfSeqDef occ=0' 
897253     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 40: 'rule getOfSeqDef' 
897254     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 41: 'rule ifthenelse_split occ=0' 
897255     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 42: 'rule andLeft occ=0' 
897255     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 43: 'rule sub_zero_2 occ=0' 
897256     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 44: 'rule ifthenelse_split occ=2' 
897257     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 45: 'rule andLeft' 
897257     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 46: 'rule sub_zero_2 occ=0' 
897257     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 47: 'rule add_zero_right occ=0' 
897258     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 48: 'rule add_zero_right occ=0' 
897259     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 49: 'rule add_zero_right occ=0' 
897259     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 50: 'rule add_zero_right occ=0' 
897260     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 51: 'rule add_zero_right occ=0' 
897260     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 52: 'rule add_zero_right occ=0' 
897261     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 53: 'rule ifthenelse_split occ=0' 
897262     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 54: 'rule ifthenelse_split occ=0' 
897263     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 55: 'tryclose branch' 
897265     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 56: 'tryclose branch' 
897305     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 57: 'rule ifthenelse_split occ=0' 
897307     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 58: 'tryclose branch' 
897363     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 59: 'rule ifthenelse_split occ=0' 
897364     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 60: 'rule seqNPermInjective' 
897366     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 61: 'instantiate hide var=iv with='iv_0'' 
897368     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 62: 'instantiate hide var=jv with='f_y'' 
897369     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 63: 'rule impLeft' 
897369     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 64: 'tryclose branch' 
897424     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 65: 'tryclose branch' 
897427     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 66: 'rule ifthenelse_split occ=0' 
897428     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 67: 'rule seqNPermInjective' 
897430     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 68: 'instantiate hide var=iv with='iv_0'' 
897431     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 69: 'instantiate hide var=jv with='f_x'' 
897432     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 70: 'rule impLeft' 
897433     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 71: 'tryclose branch' 
897487     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 72: 'tryclose branch' 
897490     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 73: 'tryclose branch' 
897496     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 74: 'tryclose branch' 
897562     INFO  Test worker     d.u.i.k.m.s.ProofScriptEngine 75: 'tryclose branch' 
901179     INFO  Test worker     d.u.i.k.t.l.TacletProofObligationInput Proof obligation for taclet: eqSameSeq