Input TRS:
    1: +(|1|(),x) -> +(+(|0|(),|1|()),x)
    2: +(|0|(),x) -> x
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... failed.
Freezing +
1: +❆1_|1|(x) -> +(+❆1_|0|(|1|()),x)
2: +❆1_|0|(x) -> x
3: +(|0|(),_1) ->= +❆1_|0|(_1)
4: +(|1|(),_1) ->= +❆1_|1|(_1)
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... removes: 3
   |0|()	weight: 0
+❆1_|1|(x1)	weight: (/ 1 2) + x1
   |1|()	weight: 0
+❆1_|0|(x1)	weight: x1
     +(x1,x2)	weight: (/ 1 2) + x1 + x2
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #+❆1_|1|(x) -> #+(+❆1_|0|(|1|()),x)
   #2: #+❆1_|1|(x) -> #+❆1_|0|(|1|())
   #3: #+(|1|(),_1) ->? #+❆1_|1|(_1)
Number of SCCs: 1, DPs: 2, edges: 2
	SCC { #1 #3 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... failed.
Removing edges: failed.
Finding a loop...  found.
  #+❆1_|1|(x_{2})	-#1->
  #+(+❆1_|0|(|1|()),x_{2})	--->*
  #+(|1|(),x_{2})	-#3->
  #+❆1_|1|(x_{2})	--->*
  #+❆1_|1|(x_{2})
  Looping with: [ x_{2} := x_{2}; ]
NO