Input TRS:
    1: perfectp(|0|()) -> false()
    2: perfectp(s(x)) -> f(x,s(|0|()),s(x),s(x))
    3: f(|0|(),y,|0|(),u) -> true()
    4: f(|0|(),y,s(z),u) -> false()
    5: f(s(x),|0|(),z,u) -> f(x,u,minus(z,s(x)),u)
    6: f(s(x),s(y),z,u) -> if(le(x,y),f(s(x),minus(y,x),z,u),f(x,u,z,u))
Number of strict rules: 6
Direct Order(PosReal,>,Poly) ... failed.
Freezing f
1: perfectp(|0|()) -> false()
2: perfectp(s(x)) -> f(x,s(|0|()),s(x),s(x))
3: f❆1_|0|(y,|0|(),u) -> true()
4: f❆1_|0|(y,s(z),u) -> false()
5: f❆1_s(x,|0|(),z,u) -> f(x,u,minus(z,s(x)),u)
6: f❆1_s(x,s(y),z,u) -> if(le(x,y),f❆1_s(x,minus(y,x),z,u),f(x,u,z,u))
7: f(|0|(),_3,_4,_5) ->= f❆1_|0|(_3,_4,_5)
8: f(s(_1),_4,_5,_6) ->= f❆1_s(_1,_4,_5,_6)
Number of strict rules: 6
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #perfectp(s(x)) -> #f(x,s(|0|()),s(x),s(x))
   #2: #f❆1_s(x,s(y),z,u) -> #f❆1_s(x,minus(y,x),z,u)
   #3: #f❆1_s(x,s(y),z,u) -> #f(x,u,z,u)
   #4: #f(|0|(),_3,_4,_5) ->? #f❆1_|0|(_3,_4,_5)
   #5: #f❆1_s(x,|0|(),z,u) -> #f(x,u,minus(z,s(x)),u)
   #6: #f(s(_1),_4,_5,_6) ->? #f❆1_s(_1,_4,_5,_6)
Number of SCCs: 1, DPs: 3, edges: 4
	SCC { #3 #5 #6 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
#f❆1_s(x1,x2,x3,x4)	weight: (/ 1 4) + x1
    le(x1,x2)	weight: 0
#f❆1_|0|(x1,x2,x3)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
 minus(x1,x2)	weight: (/ 1 4)
#perfectp(x1)	weight: 0
 false()	weight: 0
  true()	weight: 0
f❆1_s(x1,x2,x3,x4)	weight: 0
     f(x1,x2,x3,x4)	weight: 0
f❆1_|0|(x1,x2,x3)	weight: 0
    if(x1,x2,x3)	weight: 0
   #f(x1,x2,x3,x4)	weight: x1
perfectp(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #3 #5 #6
Number of SCCs: 0, DPs: 0, edges: 0
YES