Input TRS:
    1: ap(ap(map(),f),xs) -> ap(ap(ap(if(),ap(isEmpty(),xs)),f),xs)
    2: ap(ap(ap(if(),true()),f),xs) -> nil()
    3: ap(ap(ap(if(),false()),f),xs) -> ap(ap(cons(),ap(f,ap(last(),xs))),ap(ap(map(),f),ap(dropLast(),xs)))
    4: ap(isEmpty(),nil()) -> true()
    5: ap(isEmpty(),ap(ap(cons(),x),xs)) -> false()
    6: ap(last(),ap(ap(cons(),x),nil())) -> x
    7: ap(last(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap(last(),ap(ap(cons(),y),ys))
    8: ap(dropLast(),nil()) -> nil()
    9: ap(dropLast(),ap(ap(cons(),x),nil())) -> nil()
    10: ap(dropLast(),ap(ap(cons(),x),ap(ap(cons(),y),ys))) -> ap(ap(cons(),x),ap(dropLast(),ap(ap(cons(),y),ys)))
Number of strict rules: 10
Direct Order(PosReal,>,Poly) ... failed.
Freezing ap❆1_dropLast ap❆1_last ap
1: ap❆2_map(f,xs) -> ap❆3_if(ap❆1_isEmpty(xs),f,xs)
2: ap❆3_if(true(),f,xs) -> nil()
3: ap❆3_if(false(),f,xs) -> ap❆2_cons(ap(f,ap❆1_last(xs)),ap❆2_map(f,ap❆1_dropLast(xs)))
4: ap❆1_isEmpty(nil()) -> true()
5: ap❆1_isEmpty(ap❆2_cons(x,xs)) -> false()
6: ap❆1_last❆1_ap❆2_cons(x,nil()) -> x
7: ap❆1_last❆1_ap❆2_cons(x,ap❆2_cons(y,ys)) -> ap❆1_last❆1_ap❆2_cons(y,ys)
8: ap❆1_dropLast❆1_nil() -> nil()
9: ap❆1_dropLast❆1_ap❆2_cons(x,nil()) -> nil()
10: ap❆1_dropLast❆1_ap❆2_cons(x,ap❆2_cons(y,ys)) -> ap❆2_cons(x,ap❆1_dropLast❆1_ap❆2_cons(y,ys))
11: ap(if(),_1) ->= ap❆1_if(_1)
12: ap(ap❆1_if(_1),_2) ->= ap❆2_if(_1,_2)
13: ap(ap❆2_if(_1,_2),_3) ->= ap❆3_if(_1,_2,_3)
14: ap(cons(),_1) ->= ap❆1_cons(_1)
15: ap(ap❆1_cons(_1),_2) ->= ap❆2_cons(_1,_2)
16: ap(isEmpty(),_1) ->= ap❆1_isEmpty(_1)
17: ap(dropLast(),_1) ->= ap❆1_dropLast(_1)
18: ap(last(),_1) ->= ap❆1_last(_1)
19: ap(map(),_1) ->= ap❆1_map(_1)
20: ap(ap❆1_map(_1),_2) ->= ap❆2_map(_1,_2)
21: ap❆1_last(ap❆2_cons(_1,_2)) ->= ap❆1_last❆1_ap❆2_cons(_1,_2)
22: ap❆1_dropLast(nil()) ->= ap❆1_dropLast❆1_nil()
23: ap❆1_dropLast(ap❆2_cons(_1,_2)) ->= ap❆1_dropLast❆1_ap❆2_cons(_1,_2)
Number of strict rules: 10
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #ap(ap❆2_if(_1,_2),_3) ->? #ap❆3_if(_1,_2,_3)
   #2: #ap❆1_dropLast(ap❆2_cons(_1,_2)) ->? #ap❆1_dropLast❆1_ap❆2_cons(_1,_2)
   #3: #ap(ap❆1_map(_1),_2) ->? #ap❆2_map(_1,_2)
   #4: #ap❆1_last❆1_ap❆2_cons(x,ap❆2_cons(y,ys)) -> #ap❆1_last❆1_ap❆2_cons(y,ys)
   #5: #ap❆1_dropLast❆1_ap❆2_cons(x,ap❆2_cons(y,ys)) -> #ap❆1_dropLast❆1_ap❆2_cons(y,ys)
   #6: #ap❆1_dropLast(nil()) ->? #ap❆1_dropLast❆1_nil()
   #7: #ap(dropLast(),_1) ->? #ap❆1_dropLast(_1)
   #8: #ap❆1_last(ap❆2_cons(_1,_2)) ->? #ap❆1_last❆1_ap❆2_cons(_1,_2)
   #9: #ap(isEmpty(),_1) ->? #ap❆1_isEmpty(_1)
   #10: #ap❆3_if(false(),f,xs) -> #ap(f,ap❆1_last(xs))
   #11: #ap❆3_if(false(),f,xs) -> #ap❆1_last(xs)
   #12: #ap❆3_if(false(),f,xs) -> #ap❆2_map(f,ap❆1_dropLast(xs))
   #13: #ap❆3_if(false(),f,xs) -> #ap❆1_dropLast(xs)
   #14: #ap❆2_map(f,xs) -> #ap❆3_if(ap❆1_isEmpty(xs),f,xs)
   #15: #ap❆2_map(f,xs) -> #ap❆1_isEmpty(xs)
   #16: #ap(last(),_1) ->? #ap❆1_last(_1)
Number of SCCs: 3, DPs: 7, edges: 10
	SCC { #5 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
ap❆1_if(x1)	weight: 0
ap❆1_last❆1_ap❆2_cons(x1,x2)	weight: 0
ap❆1_dropLast(x1)	weight: 0
ap❆3_if(x1,x2,x3)	weight: 0
    ap(x1,x2)	weight: 0
 false()	weight: 0
isEmpty()	weight: 0
#ap❆1_dropLast(x1)	weight: 0
#ap❆1_dropLast❆1_ap❆2_cons(x1,x2)	weight: x2
ap❆1_cons(x1)	weight: 0
#ap❆1_isEmpty(x1)	weight: 0
ap❆2_map(x1,x2)	weight: 0
  true()	weight: 0
#ap❆1_last(x1)	weight: 0
ap❆1_dropLast❆1_ap❆2_cons(x1,x2)	weight: 0
    if()	weight: 0
dropLast()	weight: 0
  last()	weight: 0
   nil()	weight: 0
ap❆2_cons(x1,x2)	weight: (/ 1 2) + x2
   map()	weight: 0
ap❆2_if(x1,x2)	weight: 0
ap❆1_map(x1)	weight: 0
#ap❆2_map(x1,x2)	weight: 0
#ap❆1_dropLast❆1_nil()	weight: 0
  #ap(x1,x2)	weight: 0
ap❆1_dropLast❆1_nil()	weight: 0
  cons()	weight: 0
ap❆1_last(x1)	weight: 0
ap❆1_isEmpty(x1)	weight: 0
#ap❆3_if(x1,x2,x3)	weight: 0
#ap❆1_last❆1_ap❆2_cons(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #5
Number of SCCs: 2, DPs: 6, edges: 9
	SCC { #4 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
ap❆1_if(x1)	weight: 0
ap❆1_last❆1_ap❆2_cons(x1,x2)	weight: 0
ap❆1_dropLast(x1)	weight: 0
ap❆3_if(x1,x2,x3)	weight: 0
    ap(x1,x2)	weight: 0
 false()	weight: 0
isEmpty()	weight: 0
#ap❆1_dropLast(x1)	weight: 0
#ap❆1_dropLast❆1_ap❆2_cons(x1,x2)	weight: 0
ap❆1_cons(x1)	weight: 0
#ap❆1_isEmpty(x1)	weight: 0
ap❆2_map(x1,x2)	weight: 0
  true()	weight: 0
#ap❆1_last(x1)	weight: 0
ap❆1_dropLast❆1_ap❆2_cons(x1,x2)	weight: 0
    if()	weight: 0
dropLast()	weight: 0
  last()	weight: 0
   nil()	weight: 0
ap❆2_cons(x1,x2)	weight: (/ 1 2) + x2
   map()	weight: 0
ap❆2_if(x1,x2)	weight: 0
ap❆1_map(x1)	weight: 0
#ap❆2_map(x1,x2)	weight: 0
#ap❆1_dropLast❆1_nil()	weight: 0
  #ap(x1,x2)	weight: 0
ap❆1_dropLast❆1_nil()	weight: 0
  cons()	weight: 0
ap❆1_last(x1)	weight: 0
ap❆1_isEmpty(x1)	weight: 0
#ap❆3_if(x1,x2,x3)	weight: 0
#ap❆1_last❆1_ap❆2_cons(x1,x2)	weight: x2
    Usable rules: { }
    Removed DPs: #4
Number of SCCs: 1, DPs: 5, edges: 8
	SCC { #1 #3 #10 #12 #14 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
ap❆1_if(x1)	weight: 0
ap❆1_last❆1_ap❆2_cons(x1,x2)	weight: (/ 1 2) + x2
ap❆1_dropLast(x1)	weight: (/ 1 4)
ap❆3_if(x1,x2,x3)	weight: 0
    ap(x1,x2)	weight: 0
 false()	weight: 0
isEmpty()	weight: 0
#ap❆1_dropLast(x1)	weight: 0
#ap❆1_dropLast❆1_ap❆2_cons(x1,x2)	weight: 0
ap❆1_cons(x1)	weight: 0
#ap❆1_isEmpty(x1)	weight: 0
ap❆2_map(x1,x2)	weight: 0
  true()	weight: 0
#ap❆1_last(x1)	weight: 0
ap❆1_dropLast❆1_ap❆2_cons(x1,x2)	weight: (/ 1 2) + x2
    if()	weight: 0
dropLast()	weight: 0
  last()	weight: 0
   nil()	weight: 0
ap❆2_cons(x1,x2)	weight: (/ 1 4) + x1
   map()	weight: 0
ap❆2_if(x1,x2)	weight: (/ 1 2) + x2
ap❆1_map(x1)	weight: (/ 1 2) + x1
#ap❆2_map(x1,x2)	weight: (/ 1 4) + x1
#ap❆1_dropLast❆1_nil()	weight: 0
  #ap(x1,x2)	weight: x1
ap❆1_dropLast❆1_nil()	weight: 0
  cons()	weight: 0
ap❆1_last(x1)	weight: (/ 1 4)
ap❆1_isEmpty(x1)	weight: (/ 1 4)
#ap❆3_if(x1,x2,x3)	weight: (/ 1 4) + x2
#ap❆1_last❆1_ap❆2_cons(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #1 #3 #10
Number of SCCs: 1, DPs: 2, edges: 2
	SCC { #12 #14 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
ap❆1_if(x1)	weight: 0
ap❆1_last❆1_ap❆2_cons(x1,x2)	weight: 0
ap❆1_dropLast(x1)	weight: max{0, (- (/ 1 4)) + x1}
ap❆3_if(x1,x2,x3)	weight: 0
    ap(x1,x2)	weight: 0
 false()	weight: (/ 3 4)
isEmpty()	weight: 0
#ap❆1_dropLast(x1)	weight: 0
#ap❆1_dropLast❆1_ap❆2_cons(x1,x2)	weight: 0
ap❆1_cons(x1)	weight: 0
#ap❆1_isEmpty(x1)	weight: 0
ap❆2_map(x1,x2)	weight: 0
  true()	weight: (/ 1 4)
#ap❆1_last(x1)	weight: 0
ap❆1_dropLast❆1_ap❆2_cons(x1,x2)	weight: max{0, (/ 1 4) + x2}
    if()	weight: 0
dropLast()	weight: 0
  last()	weight: 0
   nil()	weight: 0
ap❆2_cons(x1,x2)	weight: max{0, (/ 1 2) + x2}
   map()	weight: 0
ap❆2_if(x1,x2)	weight: 0
ap❆1_map(x1)	weight: 0
#ap❆2_map(x1,x2)	weight: max{0, x2}
#ap❆1_dropLast❆1_nil()	weight: 0
  #ap(x1,x2)	weight: 0
ap❆1_dropLast❆1_nil()	weight: 0
  cons()	weight: 0
ap❆1_last(x1)	weight: 0
ap❆1_isEmpty(x1)	weight: max{0, (/ 1 4) + x1}
#ap❆3_if(x1,x2,x3)	weight: max{0, (- (/ 1 2)) + x1, x3}
#ap❆1_last❆1_ap❆2_cons(x1,x2)	weight: 0
    Usable rules: { 4 5 8..10 22 23 }
    Removed DPs: #12
Number of SCCs: 0, DPs: 0, edges: 0
YES