MAYBE
Time: 0.003940
TRS:
 {    minus(0(), y) -> 0(),
    minus(s x, 0()) -> s x,
    minus(s x, s y) -> minus(x, y),
         le(0(), y) -> true(),
       le(s x, 0()) -> false(),
       le(s x, s y) -> le(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, minus(z, s x), u),
  f(s x, s y, z, u) -> if(le(x, y), f(s x, minus(y, x), z, u), f(x, u, z, u))}
 DP:
  DP:
   {  minus#(s x, s y) -> minus#(x, y),
         le#(s x, s y) -> le#(x, y),
         perfectp# s x -> f#(x, s 0(), s x, s x),
    f#(s x, 0(), z, u) -> minus#(z, s x),
    f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u),
    f#(s x, s y, z, u) -> minus#(y, x),
    f#(s x, s y, z, u) -> le#(x, y),
    f#(s x, s y, z, u) -> if#(le(x, y), f(s x, minus(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, minus(y, x), z, u)}
  TRS:
  {    minus(0(), y) -> 0(),
     minus(s x, 0()) -> s x,
     minus(s x, s y) -> minus(x, y),
          le(0(), y) -> true(),
        le(s x, 0()) -> false(),
        le(s x, s y) -> le(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, minus(z, s x), u),
   f(s x, s y, z, u) -> if(le(x, y), f(s x, minus(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, minus(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#(le(x, y), f(s x, minus(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) -> le#(x, y))
    (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> minus#(y, x))
    (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(s x, minus(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#(le(x, y), f(s x, minus(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) -> le#(x, y))
    (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> minus#(y, x))
    (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u))
    (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, 0(), z, u) -> minus#(z, s x))
    (f#(s x, s y, z, u) -> minus#(y, x), minus#(s x, s y) -> minus#(x, y))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (f#(s x, s y, z, u) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
    (f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u), f#(s x, 0(), z, u) -> minus#(z, s x))
    (f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u))
    (f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u), f#(s x, s y, z, u) -> minus#(y, x))
    (f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u), f#(s x, s y, z, u) -> le#(x, y))
    (f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u), f#(s x, s y, z, u) -> if#(le(x, y), f(s x, minus(y, x), z, u), f(x, u, z, u)))
    (f#(s x, s y, z, u) -> f#(s x, minus(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, minus(y, x), z, u), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u))
    (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, 0(), z, u) -> minus#(z, s x))
    (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u))
    (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> minus#(y, x))
    (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> le#(x, y))
    (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> if#(le(x, y), f(s x, minus(y, x), z, u), f(x, u, z, u)))
    (f#(s x, 0(), z, u) -> f#(x, u, minus(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, minus(z, s x), u), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u))
    (f#(s x, 0(), z, u) -> minus#(z, s x), minus#(s x, s y) -> minus#(x, y))}
   STATUS:
    arrows: 0.690000
    SCCS (3):
     Scc:
      {f#(s x, 0(), z, u) -> f#(x, u, minus(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, minus(y, x), z, u)}
     Scc:
      {le#(s x, s y) -> le#(x, y)}
     Scc:
      {minus#(s x, s y) -> minus#(x, y)}
     
     
     SCC (3):
      Strict:
       {f#(s x, 0(), z, u) -> f#(x, u, minus(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, minus(y, x), z, u)}
      Weak:
      {    minus(0(), y) -> 0(),
         minus(s x, 0()) -> s x,
         minus(s x, s y) -> minus(x, y),
              le(0(), y) -> true(),
            le(s x, 0()) -> false(),
            le(s x, s y) -> le(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, minus(z, s x), u),
       f(s x, s y, z, u) -> if(le(x, y), f(s x, minus(y, x), z, u), f(x, u, z, u))}
      Open
     
     
     SCC (1):
      Strict:
       {le#(s x, s y) -> le#(x, y)}
      Weak:
      {    minus(0(), y) -> 0(),
         minus(s x, 0()) -> s x,
         minus(s x, s y) -> minus(x, y),
              le(0(), y) -> true(),
            le(s x, 0()) -> false(),
            le(s x, s y) -> le(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, minus(z, s x), u),
       f(s x, s y, z, u) -> if(le(x, y), f(s x, minus(y, x), z, u), f(x, u, z, u))}
      Open
     
     
     SCC (1):
      Strict:
       {minus#(s x, s y) -> minus#(x, y)}
      Weak:
      {    minus(0(), y) -> 0(),
         minus(s x, 0()) -> s x,
         minus(s x, s y) -> minus(x, y),
              le(0(), y) -> true(),
            le(s x, 0()) -> false(),
            le(s x, s y) -> le(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, minus(z, s x), u),
       f(s x, s y, z, u) -> if(le(x, y), f(s x, minus(y, x), z, u), f(x, u, z, u))}
      Open