MAYBE
Time: 0.008371
TRS:
 {     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:
   {     perfectp# s x -> f#(x, s 0(), s x, s x),
    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)}
  TRS:
  {     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:
   {(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) -> 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, 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#(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) -> 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) -> f#(s x, minus(y, x), z, u))}
   STATUS:
    arrows: 0.500000
    SCCS (1):
     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)}
     
     
     SCC (2):
      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)}
      Weak:
      {     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