MAYBE
Time: 0.001520
TRS:
 {        -(x, 0()) -> x,
        -(s x, s y) -> -(x, y),
         <=(0(), y) -> true(),
       <=(s x, 0()) -> false(),
       <=(s x, s y) -> <=(x, y),
   if(true(), x, y) -> x,
  if(false(), x, y) -> y,
       perfectp 0() -> false(),
       perfectp s x -> f(x, s 0(), s x, s x),
  f(0(), y, 0(), u) -> true(),
  f(0(), y, s z, u) -> false(),
  f(s x, 0(), z, u) -> f(x, u, -(z, s x), u),
  f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u))}
 DP:
  DP:
   {      -#(s x, s y) -> -#(x, y),
         <=#(s x, s y) -> <=#(x, y),
         perfectp# s x -> f#(x, s 0(), s x, s x),
    f#(s x, 0(), z, u) -> -#(z, s x),
    f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u),
    f#(s x, s y, z, u) -> -#(y, x),
    f#(s x, s y, z, u) -> <=#(x, y),
    f#(s x, s y, z, u) -> if#(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u)),
    f#(s x, s y, z, u) -> f#(x, u, z, u),
    f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u)}
  TRS:
  {        -(x, 0()) -> x,
         -(s x, s y) -> -(x, y),
          <=(0(), y) -> true(),
        <=(s x, 0()) -> false(),
        <=(s x, s y) -> <=(x, y),
    if(true(), x, y) -> x,
   if(false(), x, y) -> y,
        perfectp 0() -> false(),
        perfectp s x -> f(x, s 0(), s x, s x),
   f(0(), y, 0(), u) -> true(),
   f(0(), y, s z, u) -> false(),
   f(s x, 0(), z, u) -> f(x, u, -(z, s x), u),
   f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u))}
  EDG:
   {(perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u))
    (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> f#(x, u, z, u))
    (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> if#(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u)))
    (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> <=#(x, y))
    (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> -#(y, x))
    (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u))
    (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, 0(), z, u) -> -#(z, s x))
    (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u))
    (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(x, u, z, u))
    (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> if#(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u)))
    (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> <=#(x, y))
    (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> -#(y, x))
    (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u))
    (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, 0(), z, u) -> -#(z, s x))
    (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
    (f#(s x, s y, z, u) -> <=#(x, y), <=#(s x, s y) -> <=#(x, y))
    (f#(s x, s y, z, u) -> -#(y, x), -#(s x, s y) -> -#(x, y))
    (<=#(s x, s y) -> <=#(x, y), <=#(s x, s y) -> <=#(x, y))
    (f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u), f#(s x, 0(), z, u) -> -#(z, s x))
    (f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u), f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u))
    (f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u), f#(s x, s y, z, u) -> -#(y, x))
    (f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u), f#(s x, s y, z, u) -> <=#(x, y))
    (f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u), f#(s x, s y, z, u) -> if#(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u)))
    (f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u), f#(s x, s y, z, u) -> f#(x, u, z, u))
    (f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u), f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u))
    (f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, 0(), z, u) -> -#(z, s x))
    (f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u))
    (f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, s y, z, u) -> -#(y, x))
    (f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, s y, z, u) -> <=#(x, y))
    (f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, s y, z, u) -> if#(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u)))
    (f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, s y, z, u) -> f#(x, u, z, u))
    (f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u))
    (f#(s x, 0(), z, u) -> -#(z, s x), -#(s x, s y) -> -#(x, y))}
   STATUS:
    arrows: 0.670000
    SCCS (3):
     Scc:
      {f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u),
       f#(s x, s y, z, u) -> f#(x, u, z, u),
       f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u)}
     Scc:
      {<=#(s x, s y) -> <=#(x, y)}
     Scc:
      {-#(s x, s y) -> -#(x, y)}
     
     
     SCC (3):
      Strict:
       {f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u),
        f#(s x, s y, z, u) -> f#(x, u, z, u),
        f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u)}
      Weak:
      {        -(x, 0()) -> x,
             -(s x, s y) -> -(x, y),
              <=(0(), y) -> true(),
            <=(s x, 0()) -> false(),
            <=(s x, s y) -> <=(x, y),
        if(true(), x, y) -> x,
       if(false(), x, y) -> y,
            perfectp 0() -> false(),
            perfectp s x -> f(x, s 0(), s x, s x),
       f(0(), y, 0(), u) -> true(),
       f(0(), y, s z, u) -> false(),
       f(s x, 0(), z, u) -> f(x, u, -(z, s x), u),
       f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u))}
      Open
     
     
     SCC (1):
      Strict:
       {<=#(s x, s y) -> <=#(x, y)}
      Weak:
      {        -(x, 0()) -> x,
             -(s x, s y) -> -(x, y),
              <=(0(), y) -> true(),
            <=(s x, 0()) -> false(),
            <=(s x, s y) -> <=(x, y),
        if(true(), x, y) -> x,
       if(false(), x, y) -> y,
            perfectp 0() -> false(),
            perfectp s x -> f(x, s 0(), s x, s x),
       f(0(), y, 0(), u) -> true(),
       f(0(), y, s z, u) -> false(),
       f(s x, 0(), z, u) -> f(x, u, -(z, s x), u),
       f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u))}
      Open
     
     
     SCC (1):
      Strict:
       {-#(s x, s y) -> -#(x, y)}
      Weak:
      {        -(x, 0()) -> x,
             -(s x, s y) -> -(x, y),
              <=(0(), y) -> true(),
            <=(s x, 0()) -> false(),
            <=(s x, s y) -> <=(x, y),
        if(true(), x, y) -> x,
       if(false(), x, y) -> y,
            perfectp 0() -> false(),
            perfectp s x -> f(x, s 0(), s x, s x),
       f(0(), y, 0(), u) -> true(),
       f(0(), y, s z, u) -> false(),
       f(s x, 0(), z, u) -> f(x, u, -(z, s x), u),
       f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u))}
      Open