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.
   |0|()	weight: 0
fib❆1_|0|()	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#fib❆1_s(x1)	weight: 0
#fib❆1_|0|()	weight: 0
   fib(x1)	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.
   |0|()	weight: 0
fib❆1_|0|()	weight: 0
     s(x1)	weight: (/ 1 2) + x1
#fib❆1_s(x1)	weight: x1
#fib❆1_|0|()	weight: 0
   fib(x1)	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