MAYBE
Time: 0.003787
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}
       Open