YES
Time: 0.000723
TRS:
 {u21(ackout X, Y) -> u22 ackin(Y, X),
   ackin(s X, s Y) -> u21(ackin(s X, Y), X)}
 DP:
  DP:
   {u21#(ackout X, Y) -> ackin#(Y, X),
     ackin#(s X, s Y) -> u21#(ackin(s X, Y), X),
     ackin#(s X, s Y) -> ackin#(s X, Y)}
  TRS:
  {u21(ackout X, Y) -> u22 ackin(Y, X),
    ackin(s X, s Y) -> u21(ackin(s X, Y), X)}
  EDG:
   {(u21#(ackout X, Y) -> ackin#(Y, X), ackin#(s X, s Y) -> u21#(ackin(s X, Y), X))
    (u21#(ackout X, Y) -> ackin#(Y, X), ackin#(s X, s Y) -> ackin#(s X, Y))
    (ackin#(s X, s Y) -> ackin#(s X, Y), ackin#(s X, s Y) -> u21#(ackin(s X, Y), X))
    (ackin#(s X, s Y) -> ackin#(s X, Y), ackin#(s X, s Y) -> ackin#(s X, Y))}
   SCCS (1):
    Scc:
     {ackin#(s X, s Y) -> ackin#(s X, Y)}
    SCC (1):
     Strict:
      {ackin#(s X, s Y) -> ackin#(s X, Y)}
     Weak:
     {u21(ackout X, Y) -> u22 ackin(Y, X),
       ackin(s X, s Y) -> u21(ackin(s X, Y), X)}
     SPSC:
      Simple Projection:
       pi(ackin#) = 1
      Strict:
       {}
      Qed