YES
Time: 0.038345
TRS:
 { ack_in(s m, s n) -> u21(ack_in(s m, n), m),
   ack_in(s m, 0()) -> u11 ack_in(m, s 0()),
     ack_in(0(), n) -> ack_out s n,
      u11 ack_out n -> ack_out n,
  u21(ack_out n, m) -> u22 ack_in(m, n),
      u22 ack_out n -> ack_out n}
 DP:
  DP:
   { ack_in#(s m, s n) -> ack_in#(s m, n),
     ack_in#(s m, s n) -> u21#(ack_in(s m, n), m),
     ack_in#(s m, 0()) -> ack_in#(m, s 0()),
     ack_in#(s m, 0()) -> u11# ack_in(m, s 0()),
    u21#(ack_out n, m) -> ack_in#(m, n),
    u21#(ack_out n, m) -> u22# ack_in(m, n)}
  TRS:
  { ack_in(s m, s n) -> u21(ack_in(s m, n), m),
    ack_in(s m, 0()) -> u11 ack_in(m, s 0()),
      ack_in(0(), n) -> ack_out s n,
       u11 ack_out n -> ack_out n,
   u21(ack_out n, m) -> u22 ack_in(m, n),
       u22 ack_out n -> ack_out n}
  EDG:
   {(ack_in#(s m, 0()) -> ack_in#(m, s 0()), ack_in#(s m, s n) -> u21#(ack_in(s m, n), m))
    (ack_in#(s m, 0()) -> ack_in#(m, s 0()), ack_in#(s m, s n) -> ack_in#(s m, n))
    (ack_in#(s m, s n) -> u21#(ack_in(s m, n), m), u21#(ack_out n, m) -> u22# ack_in(m, n))
    (ack_in#(s m, s n) -> u21#(ack_in(s m, n), m), u21#(ack_out n, m) -> ack_in#(m, n))
    (ack_in#(s m, s n) -> ack_in#(s m, n), ack_in#(s m, 0()) -> u11# ack_in(m, s 0()))
    (ack_in#(s m, s n) -> ack_in#(s m, n), ack_in#(s m, 0()) -> ack_in#(m, s 0()))
    (ack_in#(s m, s n) -> ack_in#(s m, n), ack_in#(s m, s n) -> u21#(ack_in(s m, n), m))
    (ack_in#(s m, s n) -> ack_in#(s m, n), ack_in#(s m, s n) -> ack_in#(s m, n))
    (u21#(ack_out n, m) -> ack_in#(m, n), ack_in#(s m, s n) -> ack_in#(s m, n))
    (u21#(ack_out n, m) -> ack_in#(m, n), ack_in#(s m, s n) -> u21#(ack_in(s m, n), m))
    (u21#(ack_out n, m) -> ack_in#(m, n), ack_in#(s m, 0()) -> ack_in#(m, s 0()))
    (u21#(ack_out n, m) -> ack_in#(m, n), ack_in#(s m, 0()) -> u11# ack_in(m, s 0()))}
   STATUS:
    arrows: 0.666667
    SCCS (1):
     Scc:
      { ack_in#(s m, s n) -> ack_in#(s m, n),
        ack_in#(s m, s n) -> u21#(ack_in(s m, n), m),
        ack_in#(s m, 0()) -> ack_in#(m, s 0()),
       u21#(ack_out n, m) -> ack_in#(m, n)}
     
     SCC (4):
      Strict:
       { ack_in#(s m, s n) -> ack_in#(s m, n),
         ack_in#(s m, s n) -> u21#(ack_in(s m, n), m),
         ack_in#(s m, 0()) -> ack_in#(m, s 0()),
        u21#(ack_out n, m) -> ack_in#(m, n)}
      Weak:
      { ack_in(s m, s n) -> u21(ack_in(s m, n), m),
        ack_in(s m, 0()) -> u11 ack_in(m, s 0()),
          ack_in(0(), n) -> ack_out s n,
           u11 ack_out n -> ack_out n,
       u21(ack_out n, m) -> u22 ack_in(m, n),
           u22 ack_out n -> ack_out n}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [ack_in](x0, x1) = 0,
        
        [u21](x0, x1) = 0,
        
        [ack_out](x0) = x0,
        
        [s](x0) = x0 + 1,
        
        [u11](x0) = 0,
        
        [u22](x0) = 0,
        
        [0] = 1,
        
        [ack_in#](x0, x1) = x0,
        
        [u21#](x0, x1) = x0 + 1
       Strict:
        u21#(ack_out n, m) -> ack_in#(m, n)
        1 + 0n + 1m >= 0 + 0n + 1m
        ack_in#(s m, 0()) -> ack_in#(m, s 0())
        1 + 1m >= 0 + 1m
        ack_in#(s m, s n) -> u21#(ack_in(s m, n), m)
        1 + 0n + 1m >= 1 + 0n + 1m
        ack_in#(s m, s n) -> ack_in#(s m, n)
        1 + 0n + 1m >= 1 + 0n + 1m
       Weak:
        u22 ack_out n -> ack_out n
        0 + 0n >= 0 + 1n
        u21(ack_out n, m) -> u22 ack_in(m, n)
        0 + 0n + 0m >= 0 + 0n + 0m
        u11 ack_out n -> ack_out n
        0 + 0n >= 0 + 1n
        ack_in(0(), n) -> ack_out s n
        0 + 0n >= 1 + 1n
        ack_in(s m, 0()) -> u11 ack_in(m, s 0())
        0 + 0m >= 0 + 0m
        ack_in(s m, s n) -> u21(ack_in(s m, n), m)
        0 + 0n + 0m >= 0 + 0n + 0m
      SCCS (1):
       Scc:
        {ack_in#(s m, s n) -> ack_in#(s m, n)}
       
       SCC (1):
        Strict:
         {ack_in#(s m, s n) -> ack_in#(s m, n)}
        Weak:
        { ack_in(s m, s n) -> u21(ack_in(s m, n), m),
          ack_in(s m, 0()) -> u11 ack_in(m, s 0()),
            ack_in(0(), n) -> ack_out s n,
             u11 ack_out n -> ack_out n,
         u21(ack_out n, m) -> u22 ack_in(m, n),
             u22 ack_out n -> ack_out n}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [ack_in](x0, x1) = x0 + 1,
          
          [u21](x0, x1) = x0 + x1,
          
          [ack_out](x0) = x0 + 1,
          
          [s](x0) = x0 + 1,
          
          [u11](x0) = 0,
          
          [u22](x0) = x0 + 1,
          
          [0] = 1,
          
          [ack_in#](x0, x1) = x0 + 1
         Strict:
          ack_in#(s m, s n) -> ack_in#(s m, n)
          2 + 1n + 0m >= 1 + 1n + 0m
         Weak:
          u22 ack_out n -> ack_out n
          2 + 1n >= 1 + 1n
          u21(ack_out n, m) -> u22 ack_in(m, n)
          1 + 1n + 1m >= 2 + 0n + 1m
          u11 ack_out n -> ack_out n
          0 + 0n >= 1 + 1n
          ack_in(0(), n) -> ack_out s n
          2 + 0n >= 2 + 1n
          ack_in(s m, 0()) -> u11 ack_in(m, s 0())
          2 + 1m >= 0 + 0m
          ack_in(s m, s n) -> u21(ack_in(s m, n), m)
          2 + 0n + 1m >= 2 + 0n + 2m
        Qed