Input TRS:
    1: din(der(plus(X,Y))) -> u21(din(der(X)),X,Y)
    2: u21(dout(DX),X,Y) -> u22(din(der(Y)),X,Y,DX)
    3: u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
    4: din(der(times(X,Y))) -> u31(din(der(X)),X,Y)
    5: u31(dout(DX),X,Y) -> u32(din(der(Y)),X,Y,DX)
    6: u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
    7: din(der(der(X))) -> u41(din(der(X)),X)
    8: u41(dout(DX),X) -> u42(din(der(DX)),X,DX)
    9: u42(dout(DDX),X,DX) -> dout(DDX)
Number of strict rules: 9
Direct Order(PosReal,>,Poly) ... failed.
Freezing din
1: din❆1_der(plus(X,Y)) -> u21(din❆1_der(X),X,Y)
2: u21(dout(DX),X,Y) -> u22(din❆1_der(Y),X,Y,DX)
3: u22(dout(DY),X,Y,DX) -> dout(plus(DX,DY))
4: din❆1_der(times(X,Y)) -> u31(din❆1_der(X),X,Y)
5: u31(dout(DX),X,Y) -> u32(din❆1_der(Y),X,Y,DX)
6: u32(dout(DY),X,Y,DX) -> dout(plus(times(X,DY),times(Y,DX)))
7: din❆1_der(der(X)) -> u41(din❆1_der(X),X)
8: u41(dout(DX),X) -> u42(din❆1_der(DX),X,DX)
9: u42(dout(DDX),X,DX) -> dout(DDX)
10: din(der(_1)) ->= din❆1_der(_1)
Number of strict rules: 9
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #u21(dout(DX),X,Y) -> #u22(din❆1_der(Y),X,Y,DX)
   #2: #u21(dout(DX),X,Y) -> #din❆1_der(Y)
   #3: #din❆1_der(der(X)) -> #u41(din❆1_der(X),X)
   #4: #din❆1_der(der(X)) -> #din❆1_der(X)
   #5: #din(der(_1)) ->? #din❆1_der(_1)
   #6: #u31(dout(DX),X,Y) -> #u32(din❆1_der(Y),X,Y,DX)
   #7: #u31(dout(DX),X,Y) -> #din❆1_der(Y)
   #8: #din❆1_der(plus(X,Y)) -> #u21(din❆1_der(X),X,Y)
   #9: #din❆1_der(plus(X,Y)) -> #din❆1_der(X)
   #10: #u41(dout(DX),X) -> #u42(din❆1_der(DX),X,DX)
   #11: #u41(dout(DX),X) -> #din❆1_der(DX)
   #12: #din❆1_der(times(X,Y)) -> #u31(din❆1_der(X),X,Y)
   #13: #din❆1_der(times(X,Y)) -> #din❆1_der(X)
Number of SCCs: 1, DPs: 9, edges: 39
	SCC { #2..4 #7..9 #11..13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   din(x1)	weight: 0
 #u22(x1,x2,x3,x4)	weight: 0
   der(x1)	weight: (/ 1 4)
 #u21(x1,x2,x3)	weight: (/ 1 2)
 #din(x1)	weight: 0
   u41(x1,x2)	weight: x1
 times(x1,x2)	weight: (/ 1 4)
   u32(x1,x2,x3,x4)	weight: x1
   u21(x1,x2,x3)	weight: (/ 1 4)
 #u41(x1,x2)	weight: x1
  plus(x1,x2)	weight: (/ 1 4)
 #u42(x1,x2,x3)	weight: 0
 #u31(x1,x2,x3)	weight: (/ 1 2)
   u22(x1,x2,x3,x4)	weight: x1
   u42(x1,x2,x3)	weight: x1
#din❆1_der(x1)	weight: (/ 1 2)
din❆1_der(x1)	weight: (/ 1 4)
 #u32(x1,x2,x3,x4)	weight: 0
  dout(x1)	weight: (/ 3 4)
   u31(x1,x2,x3)	weight: (/ 1 4)
    Usable rules: { 1..9 }
    Removed DPs: #3 #11
Number of SCCs: 1, DPs: 7, edges: 27
	SCC { #2 #4 #7..9 #12 #13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   din(x1)	weight: 0
 #u22(x1,x2,x3,x4)	weight: 0
   der(x1)	weight: (/ 1 4)
 #u21(x1,x2,x3)	weight: (/ 1 2)
 #din(x1)	weight: 0
   u41(x1,x2)	weight: x1
 times(x1,x2)	weight: (/ 1 4)
   u32(x1,x2,x3,x4)	weight: x1
   u21(x1,x2,x3)	weight: (/ 1 4)
 #u41(x1,x2)	weight: x1
  plus(x1,x2)	weight: (/ 1 4)
 #u42(x1,x2,x3)	weight: 0
 #u31(x1,x2,x3)	weight: x1
   u22(x1,x2,x3,x4)	weight: x1
   u42(x1,x2,x3)	weight: x1
#din❆1_der(x1)	weight: (/ 1 2)
din❆1_der(x1)	weight: (/ 1 4)
 #u32(x1,x2,x3,x4)	weight: 0
  dout(x1)	weight: (/ 3 4)
   u31(x1,x2,x3)	weight: (/ 1 4)
    Usable rules: { 1..9 }
    Removed DPs: #7 #12
Number of SCCs: 1, DPs: 5, edges: 17
	SCC { #2 #4 #8 #9 #13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   din(x1)	weight: 0
 #u22(x1,x2,x3,x4)	weight: 0
   der(x1)	weight: (/ 1 8)
 #u21(x1,x2,x3)	weight: (/ 1 4) + x1
 #din(x1)	weight: 0
   u41(x1,x2)	weight: x1
 times(x1,x2)	weight: (/ 1 8)
   u32(x1,x2,x3,x4)	weight: x1
   u21(x1,x2,x3)	weight: (/ 1 8)
 #u41(x1,x2)	weight: x1
  plus(x1,x2)	weight: (/ 1 8)
 #u42(x1,x2,x3)	weight: 0
 #u31(x1,x2,x3)	weight: x1
   u22(x1,x2,x3,x4)	weight: x1
   u42(x1,x2,x3)	weight: x1
#din❆1_der(x1)	weight: (/ 1 2)
din❆1_der(x1)	weight: (/ 1 8)
 #u32(x1,x2,x3,x4)	weight: 0
  dout(x1)	weight: (/ 3 8)
   u31(x1,x2,x3)	weight: (/ 1 8)
    Usable rules: { 1..9 }
    Removed DPs: #2 #8
Number of SCCs: 1, DPs: 3, edges: 9
	SCC { #4 #9 #13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   din(x1)	weight: 0
 #u22(x1,x2,x3,x4)	weight: 0
   der(x1)	weight: (/ 1 8) + x1
 #u21(x1,x2,x3)	weight: (/ 1 4) + x1
 #din(x1)	weight: 0
   u41(x1,x2)	weight: x1
 times(x1,x2)	weight: (/ 1 8) + x1
   u32(x1,x2,x3,x4)	weight: x1
   u21(x1,x2,x3)	weight: (/ 1 8)
 #u41(x1,x2)	weight: x1
  plus(x1,x2)	weight: (/ 1 8) + x1
 #u42(x1,x2,x3)	weight: 0
 #u31(x1,x2,x3)	weight: x1
   u22(x1,x2,x3,x4)	weight: x1
   u42(x1,x2,x3)	weight: x1
#din❆1_der(x1)	weight: (/ 1 2) + x1
din❆1_der(x1)	weight: (/ 1 8)
 #u32(x1,x2,x3,x4)	weight: 0
  dout(x1)	weight: (/ 3 8)
   u31(x1,x2,x3)	weight: (/ 1 8)
    Usable rules: { }
    Removed DPs: #4 #9 #13
Number of SCCs: 0, DPs: 0, edges: 0
YES