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