Input TRS:
    1: fib(0()) -> 0()
    2: fib(s(0())) -> s(0())
    3: fib(s(s(x))) -> +(fib(s(x)),fib(x))
    4: +(x,0()) -> x
    5: +(x,s(y)) -> s(+(x,y))
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... failed.
Freezing fib
1: fib❆1_0() -> 0()
2: fib❆1_s(0()) -> s(0())
3: fib❆1_s(s(x)) -> +(fib❆1_s(x),fib(x))
4: +(x,0()) -> x
5: +(x,s(y)) -> s(+(x,y))
6: fib(0()) ->= fib❆1_0()
7: fib(s(_1)) ->= fib❆1_s(_1)
Number of strict rules: 5
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #fib(0()) ->? #fib❆1_0()
   #2: #fib(s(_1)) ->? #fib❆1_s(_1)
   #3: #+(x,s(y)) -> #+(x,y)
   #4: #fib❆1_s(s(x)) -> #+(fib❆1_s(x),fib(x))
   #5: #fib❆1_s(s(x)) -> #fib❆1_s(x)
   #6: #fib❆1_s(s(x)) -> #fib(x)
Number of SCCs: 2, DPs: 4, edges: 6
	SCC { #3 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 2) + x1
#fib❆1_s(x1)	weight: 0
fib❆1_0()	weight: 0
   fib(x1)	weight: 0
     0()	weight: 0
#fib❆1_0()	weight: 0
fib❆1_s(x1)	weight: 0
     +(x1,x2)	weight: 0
 #fib(x1)	weight: 0
   #+(x1,x2)	weight: x2
    Usable rules: { }
    Removed DPs: #3
Number of SCCs: 1, DPs: 3, edges: 5
	SCC { #2 #5 #6 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
     s(x1)	weight: (/ 1 2) + x1
#fib❆1_s(x1)	weight: x1
fib❆1_0()	weight: 0
   fib(x1)	weight: 0
     0()	weight: 0
#fib❆1_0()	weight: 0
fib❆1_s(x1)	weight: 0
     +(x1,x2)	weight: 0
 #fib(x1)	weight: x1
   #+(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #2 #5 #6
Number of SCCs: 0, DPs: 0, edges: 0
YES