Problem GTSSK07 cade15

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputGTSSK07 cade15

stdout:

MAYBE

Problem:
 sort(l) -> st(0(),l)
 st(n,l) -> cond1(member(n,l),n,l)
 cond1(true(),n,l) -> cons(n,st(s(n),l))
 cond1(false(),n,l) -> cond2(gt(n,max(l)),n,l)
 cond2(true(),n,l) -> nil()
 cond2(false(),n,l) -> st(s(n),l)
 member(n,nil()) -> false()
 member(n,cons(m,l)) -> or(equal(n,m),member(n,l))
 or(x,true()) -> true()
 or(x,false()) -> x
 equal(0(),0()) -> true()
 equal(s(x),0()) -> false()
 equal(0(),s(y)) -> false()
 equal(s(x),s(y)) -> equal(x,y)
 gt(0(),v) -> false()
 gt(s(u),0()) -> true()
 gt(s(u),s(v)) -> gt(u,v)
 max(nil()) -> 0()
 max(cons(u,l)) -> if(gt(u,max(l)),u,max(l))
 if(true(),u,v) -> u
 if(false(),u,v) -> v

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputGTSSK07 cade15

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputGTSSK07 cade15

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  sort(l) -> st(0(), l)
     , st(n, l) -> cond1(member(n, l), n, l)
     , cond1(true(), n, l) -> cons(n, st(s(n), l))
     , cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l)
     , cond2(true(), n, l) -> nil()
     , cond2(false(), n, l) -> st(s(n), l)
     , member(n, nil()) -> false()
     , member(n, cons(m, l)) -> or(equal(n, m), member(n, l))
     , or(x, true()) -> true()
     , or(x, false()) -> x
     , equal(0(), 0()) -> true()
     , equal(s(x), 0()) -> false()
     , equal(0(), s(y)) -> false()
     , equal(s(x), s(y)) -> equal(x, y)
     , gt(0(), v) -> false()
     , gt(s(u), 0()) -> true()
     , gt(s(u), s(v)) -> gt(u, v)
     , max(nil()) -> 0()
     , max(cons(u, l)) -> if(gt(u, max(l)), u, max(l))
     , if(true(), u, v) -> u
     , if(false(), u, v) -> v}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputGTSSK07 cade15

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputGTSSK07 cade15

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  sort(l) -> st(0(), l)
     , st(n, l) -> cond1(member(n, l), n, l)
     , cond1(true(), n, l) -> cons(n, st(s(n), l))
     , cond1(false(), n, l) -> cond2(gt(n, max(l)), n, l)
     , cond2(true(), n, l) -> nil()
     , cond2(false(), n, l) -> st(s(n), l)
     , member(n, nil()) -> false()
     , member(n, cons(m, l)) -> or(equal(n, m), member(n, l))
     , or(x, true()) -> true()
     , or(x, false()) -> x
     , equal(0(), 0()) -> true()
     , equal(s(x), 0()) -> false()
     , equal(0(), s(y)) -> false()
     , equal(s(x), s(y)) -> equal(x, y)
     , gt(0(), v) -> false()
     , gt(s(u), 0()) -> true()
     , gt(s(u), s(v)) -> gt(u, v)
     , max(nil()) -> 0()
     , max(cons(u, l)) -> if(gt(u, max(l)), u, max(l))
     , if(true(), u, v) -> u
     , if(false(), u, v) -> v}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds