YES
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:
  Strict:
   {      -#(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)}
  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))}
  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))
    (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))}
   SCCS:
    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:
     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))}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       { 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)}
      EDG:
       {(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), 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) -> 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) -> f#(s(x), -(y, x), z, u))}
       SCCS:
        Scc:
         { 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)}
        SCC:
         Strict:
          { 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)}
         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))}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {f#(s(x), s(y), z, u) -> f#(s(x), -(y, x), z, u)}
          EDG:
           {(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))}
           SCCS:
            Scc:
             {f#(s(x), s(y), z, u) -> f#(s(x), -(y, x), z, u)}
            SCC:
             Strict:
              {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))}
             POLY:
              Argument Filtering:
               pi(f#) = 1, pi(f) = [], pi(perfectp) = [], pi(if) = [], pi(false) = [], pi(<=) = [], pi(true) = [], pi(s) = [0], pi(0) = [], pi(-) = 0
              Usable Rules:
               {}
              Interpretation:
               [s](x0) = x0 + 1
              Strict:
               {}
              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))}
              Qed
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(<=#) = 0
      Strict:
       {}
      Qed
    SCC:
     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))}
     SPSC:
      Simple Projection:
       pi(-#) = 0
      Strict:
       {}
      Qed