MAYBE

Problem:
 din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
 u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
 u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
 din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
 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)))
 din(der(der(X))) -> u41(din(der(X)),X)
 u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
 u42(dout(DDX),X,DX) -> dout(DDX)

Proof:
 DP Processor:
  DPs:
   din#(der(plus(X,Y))) -> din#(der(X))
   din#(der(plus(X,Y))) -> u21#(din(der(X)),X,Y)
   u21#(dout(DX),X,Y) -> din#(der(Y))
   u21#(dout(DX),X,Y) -> u22#(din(der(Y)),X,Y,DX)
   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)
   din#(der(der(X))) -> din#(der(X))
   din#(der(der(X))) -> u41#(din(der(X)),X)
   u41#(dout(DX),X) -> din#(der(DX))
   u41#(dout(DX),X) -> u42#(din(der(DX)),X,DX)
  TRS:
   din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
   u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
   u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
   din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
   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)))
   din(der(der(X))) -> u41(din(der(X)),X)
   u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
   u42(dout(DDX),X,DX) -> dout(DDX)
  TDG Processor:
   DPs:
    din#(der(plus(X,Y))) -> din#(der(X))
    din#(der(plus(X,Y))) -> u21#(din(der(X)),X,Y)
    u21#(dout(DX),X,Y) -> din#(der(Y))
    u21#(dout(DX),X,Y) -> u22#(din(der(Y)),X,Y,DX)
    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)
    din#(der(der(X))) -> din#(der(X))
    din#(der(der(X))) -> u41#(din(der(X)),X)
    u41#(dout(DX),X) -> din#(der(DX))
    u41#(dout(DX),X) -> u42#(din(der(DX)),X,DX)
   TRS:
    din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
    u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
    u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
    din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
    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)))
    din(der(der(X))) -> u41(din(der(X)),X)
    u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
    u42(dout(DDX),X,DX) -> dout(DDX)
   graph:
    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(der(X))) -> din#(der(X))
    u41#(dout(DX),X) -> din#(der(DX)) ->
    din#(der(times(X,Y))) -> u31#(din(der(X)),X,Y)
    u41#(dout(DX),X) -> din#(der(DX)) ->
    din#(der(times(X,Y))) -> din#(der(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))
    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(der(X))) -> din#(der(X))
    u31#(dout(DX),X,Y) -> din#(der(Y)) ->
    din#(der(times(X,Y))) -> u31#(din(der(X)),X,Y)
    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(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))
    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))
    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))) -> u21#(din(der(X)),X,Y)
    u21#(dout(DX),X,Y) -> din#(der(Y)) ->
    din#(der(plus(X,Y))) -> din#(der(X))
    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(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(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))) -> u21#(din(der(X)),X,Y)
    din#(der(times(X,Y))) -> din#(der(X)) ->
    din#(der(plus(X,Y))) -> din#(der(X))
    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))
    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(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))) -> u21#(din(der(X)),X,Y)
    din#(der(der(X))) -> din#(der(X)) ->
    din#(der(plus(X,Y))) -> din#(der(X))
    din#(der(plus(X,Y))) -> u21#(din(der(X)),X,Y) ->
    u21#(dout(DX),X,Y) -> u22#(din(der(Y)),X,Y,DX)
    din#(der(plus(X,Y))) -> u21#(din(der(X)),X,Y) ->
    u21#(dout(DX),X,Y) -> din#(der(Y))
    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(der(X))) -> din#(der(X))
    din#(der(plus(X,Y))) -> din#(der(X)) ->
    din#(der(times(X,Y))) -> u31#(din(der(X)),X,Y)
    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(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))
   SCC Processor:
    #sccs: 1
    #rules: 9
    #arcs: 42/144
    DPs:
     u41#(dout(DX),X) -> din#(der(DX))
     din#(der(plus(X,Y))) -> din#(der(X))
     din#(der(plus(X,Y))) -> u21#(din(der(X)),X,Y)
     u21#(dout(DX),X,Y) -> din#(der(Y))
     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))
     din#(der(der(X))) -> din#(der(X))
     din#(der(der(X))) -> u41#(din(der(X)),X)
    TRS:
     din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
     u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
     u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
     din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
     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)))
     din(der(der(X))) -> u41(din(der(X)),X)
     u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
     u42(dout(DDX),X,DX) -> dout(DDX)
    Open