Input TRS:
    1: ap(ap(ff(),x),x) -> ap(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil()))
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... failed.
Freezing ap
1: ap❆2_ff(x,x) -> ap(ap(x,ap❆1_ff(x)),ap❆2_cons(x,nil()))
2: ap(cons(),_1) ->= ap❆1_cons(_1)
3: ap(ap❆1_cons(_1),_2) ->= ap❆2_cons(_1,_2)
4: ap(ff(),_1) ->= ap❆1_ff(_1)
5: ap(ap❆1_ff(_1),_2) ->= ap❆2_ff(_1,_2)
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #ap(ap❆1_ff(_1),_2) ->? #ap❆2_ff(_1,_2)
   #2: #ap❆2_ff(x,x) -> #ap(ap(x,ap❆1_ff(x)),ap❆2_cons(x,nil()))
   #3: #ap❆2_ff(x,x) -> #ap(x,ap❆1_ff(x))
Number of SCCs: 1, DPs: 3, edges: 4
	SCC { #1..3 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
#ap❆2_ff(x1,x2)	weight: max{0, (/ 1 16) + x2}
    ap(x1,x2)	weight: max{0, (- (/ 3 16)) + x1, (- (/ 1 4)) + x2}
    ff()	weight: (/ 3 8)
ap❆1_cons(x1)	weight: (max (/ 1 4) 0)
ap❆1_ff(x1)	weight: (max (/ 3 16) 0)
   nil()	weight: (/ 5 16)
ap❆2_cons(x1,x2)	weight: max{0, (- (/ 1 4)) + x2}
  #ap(x1,x2)	weight: max{0, (- (/ 1 8)) + x2 + x1}
  cons()	weight: (/ 7 16)
ap❆2_ff(x1,x2)	weight: max{0, (- (/ 1 4)) + x2}
    Usable rules: { 1..5 }
    Removed DPs: #2
Number of SCCs: 1, DPs: 2, edges: 2
	SCC { #1 #3 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#ap❆2_ff(x1,x2)	weight: (/ 1 8) + x1
    ap(x1,x2)	weight: (/ 1 4) + x2
    ff()	weight: 0
ap❆1_cons(x1)	weight: (/ 1 8)
ap❆1_ff(x1)	weight: (/ 1 4) + x1
   nil()	weight: 0
ap❆2_cons(x1,x2)	weight: 0
  #ap(x1,x2)	weight: x1
  cons()	weight: 0
ap❆2_ff(x1,x2)	weight: (/ 1 4)
    Usable rules: { }
    Removed DPs: #1 #3
Number of SCCs: 0, DPs: 0, edges: 0
YES