Input TRS:
    1: suc(1()) -> .0(1())
    2: suc(.0(x)) -> .1(x)
    3: suc(.1(x)) -> .0(suc(x))
    4: add(x,1()) -> suc(x)
    5: add(1(),y) -> suc(y)
    6: add(.0(x),.0(y)) -> .0(add(x,y))
    7: add(.1(x),.0(y)) -> .1(add(x,y))
    8: add(.0(x),.1(y)) -> .1(add(x,y))
    9: add(.1(x),.1(y)) -> .0(suc(add(x,y)))
    10: C(.0(x)) -> C(x)
    11: C(.1(x)) -> C(add(.1(x),.1(.1(x))))
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #add(.0(x),.0(y)) -> #add(x,y)
   #2: #add(.1(x),.1(y)) -> #suc(add(x,y))
   #3: #add(.1(x),.1(y)) -> #add(x,y)
   #4: #C(.1(x)) -> #C(add(.1(x),.1(.1(x))))
   #5: #C(.1(x)) -> #add(.1(x),.1(.1(x)))
   #6: #add(.1(x),.0(y)) -> #add(x,y)
   #7: #C(.0(x)) -> #C(x)
   #8: #add(1(),y) -> #suc(y)
   #9: #suc(.1(x)) -> #suc(x)
   #10: #add(.0(x),.1(y)) -> #add(x,y)
   #11: #add(x,1()) -> #suc(x)
Number of SCCs: 3, DPs: 7, edges: 20
	SCC { #9 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     1()	weight: 0
    .0(x1)	weight: 0
 #suc(x1)	weight: x1
     C(x1)	weight: 0
   #C(x1)	weight: 0
   suc(x1)	weight: 0
 #add(x1,x2)	weight: 0
   add(x1,x2)	weight: 0
    .1(x1)	weight: (/ 1 2) + x1
    Usable rules: { }
    Removed DPs: #9
Number of SCCs: 2, DPs: 6, edges: 19
	SCC { #4 #7 }
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...  failed.
MAYBE