Input TRS:
    1: times(x,plus(y,|1|())) -> plus(times(x,plus(y,times(|1|(),|0|()))),x)
    2: times(x,|1|()) -> x
    3: plus(x,|0|()) -> x
    4: times(x,|0|()) -> |0|()
Number of strict rules: 4
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #times(x,plus(y,|1|())) -> #plus(times(x,plus(y,times(|1|(),|0|()))),x)
   #2: #times(x,plus(y,|1|())) -> #times(x,plus(y,times(|1|(),|0|())))
   #3: #times(x,plus(y,|1|())) -> #plus(y,times(|1|(),|0|()))
   #4: #times(x,plus(y,|1|())) -> #times(|1|(),|0|())
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #2 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... succeeded.
   |0|()	status: []	precedence above:
#plus(x1,x2)	status: [x2]	precedence above:
#times(x1,x2)	status: [x2]	precedence above:
 times(x1,x2)	status: []	precedence above: |0| #times plus
   |1|()	status: []	precedence above: |0| #times times plus
  plus(x1,x2)	status: [x2,x1]	precedence above: |0| #times times
    Usable rules: { 3 4 }
    Removed DPs: #2
Number of SCCs: 0, DPs: 0, edges: 0
YES