Problem AProVE 06 quicksort

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputAProVE 06 quicksort

stdout:

MAYBE

Problem:
 le(0(),y) -> true()
 le(s(x),0()) -> false()
 le(s(x),s(y)) -> le(x,y)
 app(nil(),y) -> y
 app(add(n,x),y) -> add(n,app(x,y))
 low(n,nil()) -> nil()
 low(n,add(m,x)) -> if_low(le(m,n),n,add(m,x))
 if_low(true(),n,add(m,x)) -> add(m,low(n,x))
 if_low(false(),n,add(m,x)) -> low(n,x)
 high(n,nil()) -> nil()
 high(n,add(m,x)) -> if_high(le(m,n),n,add(m,x))
 if_high(true(),n,add(m,x)) -> high(n,x)
 if_high(false(),n,add(m,x)) -> add(m,high(n,x))
 head(add(n,x)) -> n
 tail(add(n,x)) -> x
 isempty(nil()) -> true()
 isempty(add(n,x)) -> false()
 quicksort(x) -> if_qs(isempty(x),low(head(x),tail(x)),head(x),high(head(x),tail(x)))
 if_qs(true(),x,n,y) -> nil()
 if_qs(false(),x,n,y) -> app(quicksort(x),add(n,quicksort(y)))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 06 quicksort

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputAProVE 06 quicksort

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  le(0(), y) -> true()
     , le(s(x), 0()) -> false()
     , le(s(x), s(y)) -> le(x, y)
     , app(nil(), y) -> y
     , app(add(n, x), y) -> add(n, app(x, y))
     , low(n, nil()) -> nil()
     , low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
     , if_low(true(), n, add(m, x)) -> add(m, low(n, x))
     , if_low(false(), n, add(m, x)) -> low(n, x)
     , high(n, nil()) -> nil()
     , high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
     , if_high(true(), n, add(m, x)) -> high(n, x)
     , if_high(false(), n, add(m, x)) -> add(m, high(n, x))
     , head(add(n, x)) -> n
     , tail(add(n, x)) -> x
     , isempty(nil()) -> true()
     , isempty(add(n, x)) -> false()
     , quicksort(x) ->
       if_qs(isempty(x),
             low(head(x), tail(x)),
             head(x),
             high(head(x), tail(x)))
     , if_qs(true(), x, n, y) -> nil()
     , if_qs(false(), x, n, y) ->
       app(quicksort(x), add(n, quicksort(y)))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 06 quicksort

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputAProVE 06 quicksort

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  le(0(), y) -> true()
     , le(s(x), 0()) -> false()
     , le(s(x), s(y)) -> le(x, y)
     , app(nil(), y) -> y
     , app(add(n, x), y) -> add(n, app(x, y))
     , low(n, nil()) -> nil()
     , low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
     , if_low(true(), n, add(m, x)) -> add(m, low(n, x))
     , if_low(false(), n, add(m, x)) -> low(n, x)
     , high(n, nil()) -> nil()
     , high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
     , if_high(true(), n, add(m, x)) -> high(n, x)
     , if_high(false(), n, add(m, x)) -> add(m, high(n, x))
     , head(add(n, x)) -> n
     , tail(add(n, x)) -> x
     , isempty(nil()) -> true()
     , isempty(add(n, x)) -> false()
     , quicksort(x) ->
       if_qs(isempty(x),
             low(head(x), tail(x)),
             head(x),
             high(head(x), tail(x)))
     , if_qs(true(), x, n, y) -> nil()
     , if_qs(false(), x, n, y) ->
       app(quicksort(x), add(n, quicksort(y)))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds