Problem GTSSK07 cade13t

LMPO

Execution Time (secs)
0.072
Answer
MAYBE
InputGTSSK07 cade13t
MAYBE

We consider the following Problem:

  Strict Trs:
    {  div(x, s(y)) -> d(x, s(y), 0())
     , d(x, s(y), z) -> cond(ge(x, z), x, y, z)
     , cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z)))
     , cond(false(), x, y, z) -> 0()
     , ge(u, 0()) -> true()
     , ge(0(), s(v)) -> false()
     , ge(s(u), s(v)) -> ge(u, v)
     , plus(n, 0()) -> n
     , plus(n, s(m)) -> s(plus(n, m))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MPO

Execution Time (secs)
0.085
Answer
MAYBE
InputGTSSK07 cade13t
MAYBE

We consider the following Problem:

  Strict Trs:
    {  div(x, s(y)) -> d(x, s(y), 0())
     , d(x, s(y), z) -> cond(ge(x, z), x, y, z)
     , cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z)))
     , cond(false(), x, y, z) -> 0()
     , ge(u, 0()) -> true()
     , ge(0(), s(v)) -> false()
     , ge(s(u), s(v)) -> ge(u, v)
     , plus(n, 0()) -> n
     , plus(n, s(m)) -> s(plus(n, m))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP*

Execution Time (secs)
0.087
Answer
MAYBE
InputGTSSK07 cade13t
MAYBE

We consider the following Problem:

  Strict Trs:
    {  div(x, s(y)) -> d(x, s(y), 0())
     , d(x, s(y), z) -> cond(ge(x, z), x, y, z)
     , cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z)))
     , cond(false(), x, y, z) -> 0()
     , ge(u, 0()) -> true()
     , ge(0(), s(v)) -> false()
     , ge(s(u), s(v)) -> ge(u, v)
     , plus(n, 0()) -> n
     , plus(n, s(m)) -> s(plus(n, m))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP* (PS)

Execution Time (secs)
0.073
Answer
MAYBE
InputGTSSK07 cade13t
MAYBE

We consider the following Problem:

  Strict Trs:
    {  div(x, s(y)) -> d(x, s(y), 0())
     , d(x, s(y), z) -> cond(ge(x, z), x, y, z)
     , cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z)))
     , cond(false(), x, y, z) -> 0()
     , ge(u, 0()) -> true()
     , ge(0(), s(v)) -> false()
     , ge(s(u), s(v)) -> ge(u, v)
     , plus(n, 0()) -> n
     , plus(n, s(m)) -> s(plus(n, m))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP*

Execution Time (secs)
0.068
Answer
MAYBE
InputGTSSK07 cade13t
MAYBE

We consider the following Problem:

  Strict Trs:
    {  div(x, s(y)) -> d(x, s(y), 0())
     , d(x, s(y), z) -> cond(ge(x, z), x, y, z)
     , cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z)))
     , cond(false(), x, y, z) -> 0()
     , ge(u, 0()) -> true()
     , ge(0(), s(v)) -> false()
     , ge(s(u), s(v)) -> ge(u, v)
     , plus(n, 0()) -> n
     , plus(n, s(m)) -> s(plus(n, m))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP* (PS)

Execution Time (secs)
0.082
Answer
MAYBE
InputGTSSK07 cade13t
MAYBE

We consider the following Problem:

  Strict Trs:
    {  div(x, s(y)) -> d(x, s(y), 0())
     , d(x, s(y), z) -> cond(ge(x, z), x, y, z)
     , cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z)))
     , cond(false(), x, y, z) -> 0()
     , ge(u, 0()) -> true()
     , ge(0(), s(v)) -> false()
     , ge(s(u), s(v)) -> ge(u, v)
     , plus(n, 0()) -> n
     , plus(n, s(m)) -> s(plus(n, m))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..