Problem AProVE 06 sizeChange

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputAProVE 06 sizeChange

stdout:

MAYBE

Problem:
 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)))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 06 sizeChange

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputAProVE 06 sizeChange

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  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)))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 06 sizeChange

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputAProVE 06 sizeChange

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  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)))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds