Input TRS:
    1: isEmpty(nil()) -> true()
    2: isEmpty(cons(x,xs)) -> false()
    3: last(cons(x,nil())) -> x
    4: last(cons(x,cons(y,ys))) -> last(cons(y,ys))
    5: dropLast(nil()) -> nil()
    6: dropLast(cons(x,nil())) -> nil()
    7: dropLast(cons(x,cons(y,ys))) -> cons(x,dropLast(cons(y,ys)))
    8: append(nil(),ys) -> ys
    9: append(cons(x,xs),ys) -> cons(x,append(xs,ys))
    10: reverse(xs) -> rev(xs,nil())
    11: rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
    12: if(true(),xs,ys,zs) -> zs
    13: if(false(),xs,ys,zs) -> rev(xs,ys)
Number of strict rules: 13
Direct Order(PosReal,>,Poly) ... failed.
Freezing last dropLast
1: isEmpty(nil()) -> true()
2: isEmpty(cons(x,xs)) -> false()
3: last❆1_cons(x,nil()) -> x
4: last❆1_cons(x,cons(y,ys)) -> last❆1_cons(y,ys)
5: dropLast❆1_nil() -> nil()
6: dropLast❆1_cons(x,nil()) -> nil()
7: dropLast❆1_cons(x,cons(y,ys)) -> cons(x,dropLast❆1_cons(y,ys))
8: append(nil(),ys) -> ys
9: append(cons(x,xs),ys) -> cons(x,append(xs,ys))
10: reverse(xs) -> rev(xs,nil())
11: rev(xs,ys) -> if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
12: if(true(),xs,ys,zs) -> zs
13: if(false(),xs,ys,zs) -> rev(xs,ys)
14: dropLast(cons(_1,_2)) ->= dropLast❆1_cons(_1,_2)
15: dropLast(nil()) ->= dropLast❆1_nil()
16: last(cons(_1,_2)) ->= last❆1_cons(_1,_2)
Number of strict rules: 13
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #if(false(),xs,ys,zs) -> #rev(xs,ys)
   #2: #append(cons(x,xs),ys) -> #append(xs,ys)
   #3: #rev(xs,ys) -> #if(isEmpty(xs),dropLast(xs),append(ys,last(xs)),ys)
   #4: #rev(xs,ys) -> #isEmpty(xs)
   #5: #rev(xs,ys) -> #dropLast(xs)
   #6: #rev(xs,ys) -> #append(ys,last(xs))
   #7: #rev(xs,ys) -> #last(xs)
   #8: #dropLast(cons(_1,_2)) ->? #dropLast❆1_cons(_1,_2)
   #9: #dropLast❆1_cons(x,cons(y,ys)) -> #dropLast❆1_cons(y,ys)
   #10: #reverse(xs) -> #rev(xs,nil())
   #11: #last(cons(_1,_2)) ->? #last❆1_cons(_1,_2)
   #12: #dropLast(nil()) ->? #dropLast❆1_nil()
   #13: #last❆1_cons(x,cons(y,ys)) -> #last❆1_cons(y,ys)
Number of SCCs: 4, DPs: 5, edges: 5
	SCC { #2 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #rev(x1,x2)	weight: 0
#append(x1,x2)	weight: x1
#reverse(x1)	weight: 0
#isEmpty(x1)	weight: 0
#last❆1_cons(x1,x2)	weight: 0
 false()	weight: 0
isEmpty(x1)	weight: 0
last❆1_cons(x1,x2)	weight: 0
reverse(x1)	weight: 0
  true()	weight: 0
#last(x1)	weight: 0
append(x1,x2)	weight: 0
    if(x1,x2,x3,x4)	weight: 0
#dropLast(x1)	weight: 0
dropLast(x1)	weight: 0
  last(x1)	weight: 0
   nil()	weight: 0
   rev(x1,x2)	weight: 0
dropLast❆1_nil()	weight: 0
#dropLast❆1_nil()	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x2
  #if(x1,x2,x3,x4)	weight: 0
dropLast❆1_cons(x1,x2)	weight: 0
#dropLast❆1_cons(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #2
Number of SCCs: 3, DPs: 4, edges: 4
	SCC { #13 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #rev(x1,x2)	weight: 0
#append(x1,x2)	weight: 0
#reverse(x1)	weight: 0
#isEmpty(x1)	weight: 0
#last❆1_cons(x1,x2)	weight: x2
 false()	weight: 0
isEmpty(x1)	weight: 0
last❆1_cons(x1,x2)	weight: 0
reverse(x1)	weight: 0
  true()	weight: 0
#last(x1)	weight: 0
append(x1,x2)	weight: 0
    if(x1,x2,x3,x4)	weight: 0
#dropLast(x1)	weight: 0
dropLast(x1)	weight: 0
  last(x1)	weight: 0
   nil()	weight: 0
   rev(x1,x2)	weight: 0
dropLast❆1_nil()	weight: 0
#dropLast❆1_nil()	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x2
  #if(x1,x2,x3,x4)	weight: 0
dropLast❆1_cons(x1,x2)	weight: 0
#dropLast❆1_cons(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #13
Number of SCCs: 2, DPs: 3, edges: 3
	SCC { #9 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #rev(x1,x2)	weight: 0
#append(x1,x2)	weight: 0
#reverse(x1)	weight: 0
#isEmpty(x1)	weight: 0
#last❆1_cons(x1,x2)	weight: 0
 false()	weight: 0
isEmpty(x1)	weight: 0
last❆1_cons(x1,x2)	weight: 0
reverse(x1)	weight: 0
  true()	weight: 0
#last(x1)	weight: 0
append(x1,x2)	weight: 0
    if(x1,x2,x3,x4)	weight: 0
#dropLast(x1)	weight: 0
dropLast(x1)	weight: 0
  last(x1)	weight: 0
   nil()	weight: 0
   rev(x1,x2)	weight: 0
dropLast❆1_nil()	weight: 0
#dropLast❆1_nil()	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x2
  #if(x1,x2,x3,x4)	weight: 0
dropLast❆1_cons(x1,x2)	weight: 0
#dropLast❆1_cons(x1,x2)	weight: x2
    Usable rules: { }
    Removed DPs: #9
Number of SCCs: 1, DPs: 2, edges: 2
	SCC { #1 #3 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... succeeded.
 #rev(x1,x2)	weight: max{0, (- (/ 1 4)) + x1}
#append(x1,x2)	weight: 0
#reverse(x1)	weight: 0
#isEmpty(x1)	weight: 0
#last❆1_cons(x1,x2)	weight: 0
 false()	weight: (/ 1 4)
isEmpty(x1)	weight: max{0, (- (/ 1 4)) + x1}
last❆1_cons(x1,x2)	weight: 0
reverse(x1)	weight: 0
  true()	weight: 0
#last(x1)	weight: 0
append(x1,x2)	weight: max{0, (- (/ 1 4)) + x1, x2}
    if(x1,x2,x3,x4)	weight: 0
#dropLast(x1)	weight: 0
dropLast(x1)	weight: max{0, (- (/ 1 4)) + x1}
  last(x1)	weight: (max (/ 1 4) 0)
   nil()	weight: 0
   rev(x1,x2)	weight: 0
dropLast❆1_nil()	weight: 0
#dropLast❆1_nil()	weight: 0
  cons(x1,x2)	weight: max{0, (/ 1 2) + x2}
  #if(x1,x2,x3,x4)	weight: max{0, x1, x2}
dropLast❆1_cons(x1,x2)	weight: max{0, (/ 1 4) + x2}
#dropLast❆1_cons(x1,x2)	weight: 0
    Usable rules: { 1 2 5..7 14 15 }
    Removed DPs: #1
Number of SCCs: 0, DPs: 0, edges: 0
YES