YES
Time: 0.017644
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))
    (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 (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))}
     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 (1):
        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 (2):
         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 (1):
            Scc:
             {f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u)}
            SCC (1):
             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:
              Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
              Interpretation:
               [f](x0, x1, x2, x3) = x0,
               
               [if](x0, x1, x2) = x0 + 1,
               
               [-](x0, x1) = x0,
               
               [<=](x0, x1) = x0 + 1,
               
               [s](x0) = x0 + 1,
               
               [perfectp](x0) = x0 + 1,
               
               [0] = 1,
               
               [true] = 1,
               
               [false] = 1,
               
               [f#](x0, x1, x2, x3) = x0 + x1 + 1
              Strict:
               f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u)
               3 + 1x + 1y + 0u + 0z >= 2 + 1x + 1y + 0u + 0z
              Weak:
               
             Qed
   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))}
    SPSC:
     Simple Projection:
      pi(<=#) = 1
     Strict:
      {}
     Qed
   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))}
    SPSC:
     Simple Projection:
      pi(-#) = 1
     Strict:
      {}
     Qed