YES
Time: 0.082026
TRS:
 {    u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
           din der der X -> u41(din der X, X),
      din der plus(X, Y) -> u21(din der X, X, Y),
     din der times(X, Y) -> u31(din der X, X, Y),
  u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
      u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
  u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
         u41(dout DX, X) -> u42(din der DX, X, DX),
    u42(dout DDX, X, DX) -> dout DDX}
 DP:
  DP:
   { u21#(dout DX, X, Y) -> din# der Y,
     u21#(dout DX, X, Y) -> u22#(din der Y, X, Y, DX),
          din# der der X -> din# der X,
          din# der der X -> u41#(din der X, X),
     din# der plus(X, Y) -> u21#(din der X, X, Y),
     din# der plus(X, Y) -> din# der X,
    din# der times(X, Y) -> din# der X,
    din# der times(X, Y) -> u31#(din der X, X, Y),
     u31#(dout DX, X, Y) -> din# der Y,
     u31#(dout DX, X, Y) -> u32#(din der Y, X, Y, DX),
        u41#(dout DX, X) -> din# der DX,
        u41#(dout DX, X) -> u42#(din der DX, X, DX)}
  TRS:
  {    u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
            din der der X -> u41(din der X, X),
       din der plus(X, Y) -> u21(din der X, X, Y),
      din der times(X, Y) -> u31(din der X, X, Y),
   u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
       u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
   u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
          u41(dout DX, X) -> u42(din der DX, X, DX),
     u42(dout DDX, X, DX) -> dout DDX}
  UR:
   {    u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
             din der der X -> u41(din der X, X),
        din der plus(X, Y) -> u21(din der X, X, Y),
       din der times(X, Y) -> u31(din der X, X, Y),
    u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
        u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
    u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
           u41(dout DX, X) -> u42(din der DX, X, DX),
      u42(dout DDX, X, DX) -> dout DDX,
                   a(x, y) -> x,
                   a(x, y) -> y}
   EDG:
    {(din# der times(X, Y) -> u31#(din der X, X, Y), u31#(dout DX, X, Y) -> u32#(din der Y, X, Y, DX))
     (din# der times(X, Y) -> u31#(din der X, X, Y), u31#(dout DX, X, Y) -> din# der Y)
     (din# der der X -> u41#(din der X, X), u41#(dout DX, X) -> u42#(din der DX, X, DX))
     (din# der der X -> u41#(din der X, X), u41#(dout DX, X) -> din# der DX)
     (u21#(dout DX, X, Y) -> din# der Y, din# der times(X, Y) -> u31#(din der X, X, Y))
     (u21#(dout DX, X, Y) -> din# der Y, din# der times(X, Y) -> din# der X)
     (u21#(dout DX, X, Y) -> din# der Y, din# der plus(X, Y) -> din# der X)
     (u21#(dout DX, X, Y) -> din# der Y, din# der plus(X, Y) -> u21#(din der X, X, Y))
     (u21#(dout DX, X, Y) -> din# der Y, din# der der X -> u41#(din der X, X))
     (u21#(dout DX, X, Y) -> din# der Y, din# der der X -> din# der X)
     (din# der der X -> din# der X, din# der times(X, Y) -> u31#(din der X, X, Y))
     (din# der der X -> din# der X, din# der times(X, Y) -> din# der X)
     (din# der der X -> din# der X, din# der plus(X, Y) -> din# der X)
     (din# der der X -> din# der X, din# der plus(X, Y) -> u21#(din der X, X, Y))
     (din# der der X -> din# der X, din# der der X -> u41#(din der X, X))
     (din# der der X -> din# der X, din# der der X -> din# der X)
     (din# der times(X, Y) -> din# der X, din# der times(X, Y) -> u31#(din der X, X, Y))
     (din# der times(X, Y) -> din# der X, din# der times(X, Y) -> din# der X)
     (din# der times(X, Y) -> din# der X, din# der plus(X, Y) -> din# der X)
     (din# der times(X, Y) -> din# der X, din# der plus(X, Y) -> u21#(din der X, X, Y))
     (din# der times(X, Y) -> din# der X, din# der der X -> u41#(din der X, X))
     (din# der times(X, Y) -> din# der X, din# der der X -> din# der X)
     (din# der plus(X, Y) -> din# der X, din# der der X -> din# der X)
     (din# der plus(X, Y) -> din# der X, din# der der X -> u41#(din der X, X))
     (din# der plus(X, Y) -> din# der X, din# der plus(X, Y) -> u21#(din der X, X, Y))
     (din# der plus(X, Y) -> din# der X, din# der plus(X, Y) -> din# der X)
     (din# der plus(X, Y) -> din# der X, din# der times(X, Y) -> din# der X)
     (din# der plus(X, Y) -> din# der X, din# der times(X, Y) -> u31#(din der X, X, Y))
     (u31#(dout DX, X, Y) -> din# der Y, din# der der X -> din# der X)
     (u31#(dout DX, X, Y) -> din# der Y, din# der der X -> u41#(din der X, X))
     (u31#(dout DX, X, Y) -> din# der Y, din# der plus(X, Y) -> u21#(din der X, X, Y))
     (u31#(dout DX, X, Y) -> din# der Y, din# der plus(X, Y) -> din# der X)
     (u31#(dout DX, X, Y) -> din# der Y, din# der times(X, Y) -> din# der X)
     (u31#(dout DX, X, Y) -> din# der Y, din# der times(X, Y) -> u31#(din der X, X, Y))
     (u41#(dout DX, X) -> din# der DX, din# der der X -> din# der X)
     (u41#(dout DX, X) -> din# der DX, din# der der X -> u41#(din der X, X))
     (u41#(dout DX, X) -> din# der DX, din# der plus(X, Y) -> u21#(din der X, X, Y))
     (u41#(dout DX, X) -> din# der DX, din# der plus(X, Y) -> din# der X)
     (u41#(dout DX, X) -> din# der DX, din# der times(X, Y) -> din# der X)
     (u41#(dout DX, X) -> din# der DX, din# der times(X, Y) -> u31#(din der X, X, Y))
     (din# der plus(X, Y) -> u21#(din der X, X, Y), u21#(dout DX, X, Y) -> din# der Y)
     (din# der plus(X, Y) -> u21#(din der X, X, Y), u21#(dout DX, X, Y) -> u22#(din der Y, X, Y, DX))}
    STATUS:
     arrows: 0.708333
     SCCS (1):
      Scc:
       { u21#(dout DX, X, Y) -> din# der Y,
              din# der der X -> din# der X,
              din# der der X -> u41#(din der X, X),
         din# der plus(X, Y) -> u21#(din der X, X, Y),
         din# der plus(X, Y) -> din# der X,
        din# der times(X, Y) -> din# der X,
        din# der times(X, Y) -> u31#(din der X, X, Y),
         u31#(dout DX, X, Y) -> din# der Y,
            u41#(dout DX, X) -> din# der DX}
      
      SCC (9):
       Strict:
        { u21#(dout DX, X, Y) -> din# der Y,
               din# der der X -> din# der X,
               din# der der X -> u41#(din der X, X),
          din# der plus(X, Y) -> u21#(din der X, X, Y),
          din# der plus(X, Y) -> din# der X,
         din# der times(X, Y) -> din# der X,
         din# der times(X, Y) -> u31#(din der X, X, Y),
          u31#(dout DX, X, Y) -> din# der Y,
             u41#(dout DX, X) -> din# der DX}
       Weak:
       {    u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
                 din der der X -> u41(din der X, X),
            din der plus(X, Y) -> u21(din der X, X, Y),
           din der times(X, Y) -> u31(din der X, X, Y),
        u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
            u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
        u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
               u41(dout DX, X) -> u42(din der DX, X, DX),
          u42(dout DDX, X, DX) -> dout DDX}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [u22](x0, x1, x2, x3) = x0,
         
         [u32](x0, x1, x2, x3) = x0,
         
         [u21](x0, x1, x2) = 0,
         
         [u31](x0, x1, x2) = 0,
         
         [u42](x0, x1, x2) = x0,
         
         [plus](x0, x1) = 0,
         
         [times](x0, x1) = 0,
         
         [u41](x0, x1) = 0,
         
         [din](x0) = 0,
         
         [der](x0) = 0,
         
         [dout](x0) = 1,
         
         [u21#](x0, x1, x2) = 1,
         
         [u31#](x0, x1, x2) = 1,
         
         [u41#](x0, x1) = x0 + 1,
         
         [din#](x0) = 1
        Strict:
         u41#(dout DX, X) -> din# der DX
         2 + 0X + 0DX >= 1 + 0DX
         u31#(dout DX, X, Y) -> din# der Y
         1 + 0X + 0Y + 0DX >= 1 + 0Y
         din# der times(X, Y) -> u31#(din der X, X, Y)
         1 + 0X + 0Y >= 1 + 0X + 0Y
         din# der times(X, Y) -> din# der X
         1 + 0X + 0Y >= 1 + 0X
         din# der plus(X, Y) -> din# der X
         1 + 0X + 0Y >= 1 + 0X
         din# der plus(X, Y) -> u21#(din der X, X, Y)
         1 + 0X + 0Y >= 1 + 0X + 0Y
         din# der der X -> u41#(din der X, X)
         1 + 0X >= 1 + 0X
         din# der der X -> din# der X
         1 + 0X >= 1 + 0X
         u21#(dout DX, X, Y) -> din# der Y
         1 + 0X + 0Y + 0DX >= 1 + 0Y
        Weak:
         u42(dout DDX, X, DX) -> dout DDX
         1 + 0X + 0DX + 0DDX >= 1 + 0DDX
         u41(dout DX, X) -> u42(din der DX, X, DX)
         0 + 0X + 0DX >= 0 + 0X + 0DX
         u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX))
         1 + 0X + 0Y + 0DX + 0DY >= 1 + 0X + 0Y + 0DX + 0DY
         u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX)
         0 + 0X + 0Y + 0DX >= 0 + 0X + 0Y + 0DX
         u22(dout DY, X, Y, DX) -> dout plus(DX, DY)
         1 + 0X + 0Y + 0DX + 0DY >= 1 + 0DX + 0DY
         din der times(X, Y) -> u31(din der X, X, Y)
         0 + 0X + 0Y >= 0 + 0X + 0Y
         din der plus(X, Y) -> u21(din der X, X, Y)
         0 + 0X + 0Y >= 0 + 0X + 0Y
         din der der X -> u41(din der X, X)
         0 + 0X >= 0 + 0X
         u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX)
         0 + 0X + 0Y + 0DX >= 0 + 0X + 0Y + 0DX
       SCCS (1):
        Scc:
         { u21#(dout DX, X, Y) -> din# der Y,
                din# der der X -> din# der X,
           din# der plus(X, Y) -> u21#(din der X, X, Y),
           din# der plus(X, Y) -> din# der X,
          din# der times(X, Y) -> din# der X,
          din# der times(X, Y) -> u31#(din der X, X, Y),
           u31#(dout DX, X, Y) -> din# der Y}
        
        SCC (7):
         Strict:
          { u21#(dout DX, X, Y) -> din# der Y,
                 din# der der X -> din# der X,
            din# der plus(X, Y) -> u21#(din der X, X, Y),
            din# der plus(X, Y) -> din# der X,
           din# der times(X, Y) -> din# der X,
           din# der times(X, Y) -> u31#(din der X, X, Y),
            u31#(dout DX, X, Y) -> din# der Y}
         Weak:
         {    u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
                   din der der X -> u41(din der X, X),
              din der plus(X, Y) -> u21(din der X, X, Y),
             din der times(X, Y) -> u31(din der X, X, Y),
          u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
              u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
          u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
                 u41(dout DX, X) -> u42(din der DX, X, DX),
            u42(dout DDX, X, DX) -> dout DDX}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [u22](x0, x1, x2, x3) = x0,
           
           [u32](x0, x1, x2, x3) = x0 + 1,
           
           [u21](x0, x1, x2) = 0,
           
           [u31](x0, x1, x2) = x0,
           
           [u42](x0, x1, x2) = x0,
           
           [plus](x0, x1) = x0,
           
           [times](x0, x1) = 0,
           
           [u41](x0, x1) = 0,
           
           [din](x0) = 0,
           
           [der](x0) = 0,
           
           [dout](x0) = x0 + 1,
           
           [u21#](x0, x1, x2) = 0,
           
           [u31#](x0, x1, x2) = x0,
           
           [din#](x0) = 0
          Strict:
           u31#(dout DX, X, Y) -> din# der Y
           1 + 0X + 0Y + 1DX >= 0 + 0Y
           din# der times(X, Y) -> u31#(din der X, X, Y)
           0 + 0X + 0Y >= 0 + 0X + 0Y
           din# der times(X, Y) -> din# der X
           0 + 0X + 0Y >= 0 + 0X
           din# der plus(X, Y) -> din# der X
           0 + 0X + 0Y >= 0 + 0X
           din# der plus(X, Y) -> u21#(din der X, X, Y)
           0 + 0X + 0Y >= 0 + 0X + 0Y
           din# der der X -> din# der X
           0 + 0X >= 0 + 0X
           u21#(dout DX, X, Y) -> din# der Y
           0 + 0X + 0Y + 0DX >= 0 + 0Y
          Weak:
           u42(dout DDX, X, DX) -> dout DDX
           1 + 0X + 0DX + 1DDX >= 1 + 1DDX
           u41(dout DX, X) -> u42(din der DX, X, DX)
           0 + 0X + 0DX >= 0 + 0X + 0DX
           u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX))
           2 + 0X + 0Y + 0DX + 1DY >= 1 + 0X + 0Y + 0DX + 0DY
           u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX)
           1 + 0X + 0Y + 1DX >= 1 + 0X + 0Y + 0DX
           u22(dout DY, X, Y, DX) -> dout plus(DX, DY)
           1 + 0X + 0Y + 0DX + 1DY >= 1 + 0DX + 1DY
           din der times(X, Y) -> u31(din der X, X, Y)
           0 + 0X + 0Y >= 0 + 0X + 0Y
           din der plus(X, Y) -> u21(din der X, X, Y)
           0 + 0X + 0Y >= 0 + 0X + 0Y
           din der der X -> u41(din der X, X)
           0 + 0X >= 0 + 0X
           u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX)
           0 + 0X + 0Y + 0DX >= 0 + 0X + 0Y + 0DX
         SCCS (1):
          Scc:
           { u21#(dout DX, X, Y) -> din# der Y,
                  din# der der X -> din# der X,
             din# der plus(X, Y) -> u21#(din der X, X, Y),
             din# der plus(X, Y) -> din# der X,
            din# der times(X, Y) -> din# der X}
          
          SCC (5):
           Strict:
            { u21#(dout DX, X, Y) -> din# der Y,
                   din# der der X -> din# der X,
              din# der plus(X, Y) -> u21#(din der X, X, Y),
              din# der plus(X, Y) -> din# der X,
             din# der times(X, Y) -> din# der X}
           Weak:
           {    u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
                     din der der X -> u41(din der X, X),
                din der plus(X, Y) -> u21(din der X, X, Y),
               din der times(X, Y) -> u31(din der X, X, Y),
            u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
                u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
            u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
                   u41(dout DX, X) -> u42(din der DX, X, DX),
              u42(dout DDX, X, DX) -> dout DDX}
           POLY:
            Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
            Interpretation:
             [u22](x0, x1, x2, x3) = x0 + x1,
             
             [u32](x0, x1, x2, x3) = x0 + x1,
             
             [u21](x0, x1, x2) = x0 + x1,
             
             [u31](x0, x1, x2) = x0 + x1,
             
             [u42](x0, x1, x2) = x0 + x1,
             
             [plus](x0, x1) = x0 + x1,
             
             [times](x0, x1) = x0 + 1,
             
             [u41](x0, x1) = x0 + x1,
             
             [din](x0) = x0,
             
             [der](x0) = x0,
             
             [dout](x0) = 0,
             
             [u21#](x0, x1, x2) = x0,
             
             [din#](x0) = x0
            Strict:
             din# der times(X, Y) -> din# der X
             1 + 1X + 0Y >= 0 + 1X
             din# der plus(X, Y) -> din# der X
             0 + 1X + 1Y >= 0 + 1X
             din# der plus(X, Y) -> u21#(din der X, X, Y)
             0 + 1X + 1Y >= 0 + 0X + 1Y
             din# der der X -> din# der X
             0 + 1X >= 0 + 1X
             u21#(dout DX, X, Y) -> din# der Y
             0 + 0X + 1Y + 0DX >= 0 + 1Y
            Weak:
             u42(dout DDX, X, DX) -> dout DDX
             0 + 0X + 1DX + 0DDX >= 0 + 0DDX
             u41(dout DX, X) -> u42(din der DX, X, DX)
             0 + 1X + 0DX >= 0 + 0X + 2DX
             u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX))
             0 + 0X + 1Y + 0DX + 0DY >= 0 + 0X + 0Y + 0DX + 0DY
             u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX)
             0 + 1X + 0Y + 0DX >= 0 + 0X + 2Y + 0DX
             u22(dout DY, X, Y, DX) -> dout plus(DX, DY)
             0 + 0X + 1Y + 0DX + 0DY >= 0 + 0DX + 0DY
             din der times(X, Y) -> u31(din der X, X, Y)
             1 + 1X + 0Y >= 0 + 2X + 0Y
             din der plus(X, Y) -> u21(din der X, X, Y)
             0 + 1X + 1Y >= 0 + 2X + 0Y
             din der der X -> u41(din der X, X)
             0 + 1X >= 0 + 2X
             u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX)
             0 + 1X + 0Y + 0DX >= 0 + 0X + 2Y + 0DX
           SCCS (1):
            Scc:
             {u21#(dout DX, X, Y) -> din# der Y,
                   din# der der X -> din# der X,
              din# der plus(X, Y) -> u21#(din der X, X, Y),
              din# der plus(X, Y) -> din# der X}
            
            SCC (4):
             Strict:
              {u21#(dout DX, X, Y) -> din# der Y,
                    din# der der X -> din# der X,
               din# der plus(X, Y) -> u21#(din der X, X, Y),
               din# der plus(X, Y) -> din# der X}
             Weak:
             {    u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX),
                       din der der X -> u41(din der X, X),
                  din der plus(X, Y) -> u21(din der X, X, Y),
                 din der times(X, Y) -> u31(din der X, X, Y),
              u22(dout DY, X, Y, DX) -> dout plus(DX, DY),
                  u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX),
              u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX)),
                     u41(dout DX, X) -> u42(din der DX, X, DX),
                u42(dout DDX, X, DX) -> dout DDX}
             POLY:
              Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
              Interpretation:
               [u22](x0, x1, x2, x3) = 0,
               
               [u32](x0, x1, x2, x3) = 0,
               
               [u21](x0, x1, x2) = x0 + 1,
               
               [u31](x0, x1, x2) = 0,
               
               [u42](x0, x1, x2) = 0,
               
               [plus](x0, x1) = x0 + x1 + 1,
               
               [times](x0, x1) = 0,
               
               [u41](x0, x1) = 0,
               
               [din](x0) = 0,
               
               [der](x0) = x0 + 1,
               
               [dout](x0) = 1,
               
               [u21#](x0, x1, x2) = x0 + 1,
               
               [din#](x0) = x0
              Strict:
               din# der plus(X, Y) -> din# der X
               2 + 1X + 1Y >= 1 + 1X
               din# der plus(X, Y) -> u21#(din der X, X, Y)
               2 + 1X + 1Y >= 1 + 0X + 1Y
               din# der der X -> din# der X
               2 + 1X >= 1 + 1X
               u21#(dout DX, X, Y) -> din# der Y
               1 + 0X + 1Y + 0DX >= 1 + 1Y
              Weak:
               u42(dout DDX, X, DX) -> dout DDX
               0 + 0X + 0DX + 0DDX >= 1 + 0DDX
               u41(dout DX, X) -> u42(din der DX, X, DX)
               0 + 0X + 0DX >= 0 + 0X + 0DX
               u32(dout DY, X, Y, DX) -> dout plus(times(X, DY), times(Y, DX))
               0 + 0X + 0Y + 0DX + 0DY >= 1 + 0X + 0Y + 0DX + 0DY
               u31(dout DX, X, Y) -> u32(din der Y, X, Y, DX)
               0 + 0X + 0Y + 0DX >= 0 + 0X + 0Y + 0DX
               u22(dout DY, X, Y, DX) -> dout plus(DX, DY)
               0 + 0X + 0Y + 0DX + 0DY >= 1 + 0DX + 0DY
               din der times(X, Y) -> u31(din der X, X, Y)
               0 + 0X + 0Y >= 0 + 0X + 0Y
               din der plus(X, Y) -> u21(din der X, X, Y)
               0 + 0X + 0Y >= 1 + 0X + 0Y
               din der der X -> u41(din der X, X)
               0 + 0X >= 0 + 0X
               u21(dout DX, X, Y) -> u22(din der Y, X, Y, DX)
               2 + 0X + 0Y + 0DX >= 0 + 0X + 0Y + 0DX
             SCCS (0):