Problem AProVE 06 sizeChange

LMPO

Execution Time (secs)
0.105
Answer
MAYBE
InputAProVE 06 sizeChange
MAYBE

We consider the following Problem:

  Strict Trs:
    {  r(xs, ys, zs, nil()) -> xs
     , r(xs, nil(), zs, cons(w, ws)) ->
       r(xs, xs, cons(succ(zero()), zs), ws)
     , r(xs, cons(y, ys), nil(), cons(w, ws)) ->
       r(xs, xs, cons(succ(zero()), nil()), ws)
     , r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) ->
       r(ys, cons(y, ys), zs, cons(succ(zero()), cons(w, ws)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MPO

Execution Time (secs)
0.139
Answer
MAYBE
InputAProVE 06 sizeChange
MAYBE

We consider the following Problem:

  Strict Trs:
    {  r(xs, ys, zs, nil()) -> xs
     , r(xs, nil(), zs, cons(w, ws)) ->
       r(xs, xs, cons(succ(zero()), zs), ws)
     , r(xs, cons(y, ys), nil(), cons(w, ws)) ->
       r(xs, xs, cons(succ(zero()), nil()), ws)
     , r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) ->
       r(ys, cons(y, ys), zs, cons(succ(zero()), cons(w, ws)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP*

Execution Time (secs)
0.130
Answer
MAYBE
InputAProVE 06 sizeChange
MAYBE

We consider the following Problem:

  Strict Trs:
    {  r(xs, ys, zs, nil()) -> xs
     , r(xs, nil(), zs, cons(w, ws)) ->
       r(xs, xs, cons(succ(zero()), zs), ws)
     , r(xs, cons(y, ys), nil(), cons(w, ws)) ->
       r(xs, xs, cons(succ(zero()), nil()), ws)
     , r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) ->
       r(ys, cons(y, ys), zs, cons(succ(zero()), cons(w, ws)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP* (PS)

Execution Time (secs)
0.114
Answer
MAYBE
InputAProVE 06 sizeChange
MAYBE

We consider the following Problem:

  Strict Trs:
    {  r(xs, ys, zs, nil()) -> xs
     , r(xs, nil(), zs, cons(w, ws)) ->
       r(xs, xs, cons(succ(zero()), zs), ws)
     , r(xs, cons(y, ys), nil(), cons(w, ws)) ->
       r(xs, xs, cons(succ(zero()), nil()), ws)
     , r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) ->
       r(ys, cons(y, ys), zs, cons(succ(zero()), cons(w, ws)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP*

Execution Time (secs)
0.103
Answer
MAYBE
InputAProVE 06 sizeChange
MAYBE

We consider the following Problem:

  Strict Trs:
    {  r(xs, ys, zs, nil()) -> xs
     , r(xs, nil(), zs, cons(w, ws)) ->
       r(xs, xs, cons(succ(zero()), zs), ws)
     , r(xs, cons(y, ys), nil(), cons(w, ws)) ->
       r(xs, xs, cons(succ(zero()), nil()), ws)
     , r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) ->
       r(ys, cons(y, ys), zs, cons(succ(zero()), cons(w, ws)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP* (PS)

Execution Time (secs)
0.127
Answer
MAYBE
InputAProVE 06 sizeChange
MAYBE

We consider the following Problem:

  Strict Trs:
    {  r(xs, ys, zs, nil()) -> xs
     , r(xs, nil(), zs, cons(w, ws)) ->
       r(xs, xs, cons(succ(zero()), zs), ws)
     , r(xs, cons(y, ys), nil(), cons(w, ws)) ->
       r(xs, xs, cons(succ(zero()), nil()), ws)
     , r(xs, cons(y, ys), cons(z, zs), cons(w, ws)) ->
       r(ys, cons(y, ys), zs, cons(succ(zero()), cons(w, ws)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..