Input TRS:
    1: app(app(app(compose(),f),g),x) -> app(g,app(f,x))
    2: app(reverse(),l) -> app(app(reverse2(),l),nil())
    3: app(app(reverse2(),nil()),l) -> l
    4: app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l))
    5: app(hd(),app(app(cons(),x),xs)) -> x
    6: app(tl(),app(app(cons(),x),xs)) -> xs
    7: last() -> app(app(compose(),hd()),reverse())
    8: init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse()))
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... failed.
Freezing app
1: app❆3_compose(f,g,x) -> app(g,app(f,x))
2: app❆1_reverse(l) -> app❆2_reverse2(l,nil())
3: app❆2_reverse2(nil(),l) -> l
4: app❆2_reverse2(app❆2_cons(x,xs),l) -> app❆2_reverse2(xs,app❆2_cons(x,l))
5: app❆1_hd(app❆2_cons(x,xs)) -> x
6: app❆1_tl(app❆2_cons(x,xs)) -> xs
7: last() -> app❆2_compose(hd(),reverse())
8: init() -> app❆2_compose(reverse(),app❆2_compose(tl(),reverse()))
9: app(reverse2(),_1) ->= app❆1_reverse2(_1)
10: app(app❆1_reverse2(_1),_2) ->= app❆2_reverse2(_1,_2)
11: app(cons(),_1) ->= app❆1_cons(_1)
12: app(app❆1_cons(_1),_2) ->= app❆2_cons(_1,_2)
13: app(hd(),_1) ->= app❆1_hd(_1)
14: app(tl(),_1) ->= app❆1_tl(_1)
15: app(reverse(),_1) ->= app❆1_reverse(_1)
16: app(compose(),_1) ->= app❆1_compose(_1)
17: app(app❆1_compose(_1),_2) ->= app❆2_compose(_1,_2)
18: app(app❆2_compose(_1,_2),_3) ->= app❆3_compose(_1,_2,_3)
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #app❆1_reverse(l) -> #app❆2_reverse2(l,nil())
   #2: #app(hd(),_1) ->? #app❆1_hd(_1)
   #3: #app(tl(),_1) ->? #app❆1_tl(_1)
   #4: #app(app❆1_reverse2(_1),_2) ->? #app❆2_reverse2(_1,_2)
   #5: #app❆3_compose(f,g,x) -> #app(g,app(f,x))
   #6: #app❆3_compose(f,g,x) -> #app(f,x)
   #7: #app(reverse(),_1) ->? #app❆1_reverse(_1)
   #8: #app❆2_reverse2(app❆2_cons(x,xs),l) -> #app❆2_reverse2(xs,app❆2_cons(x,l))
   #9: #app(app❆2_compose(_1,_2),_3) ->? #app❆3_compose(_1,_2,_3)
Number of SCCs: 2, DPs: 4, edges: 5
	SCC { #8 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#app❆2_reverse2(x1,x2)	weight: x1
    hd()	weight: 0
app❆1_reverse(x1)	weight: 0
app❆1_hd(x1)	weight: 0
  init()	weight: 0
#init()	weight: 0
app❆3_compose(x1,x2,x3)	weight: 0
#app❆1_tl(x1)	weight: 0
reverse2()	weight: 0
app❆2_compose(x1,x2)	weight: 0
reverse()	weight: 0
app❆2_reverse2(x1,x2)	weight: 0
compose()	weight: 0
#last()	weight: 0
app❆1_compose(x1)	weight: 0
    tl()	weight: 0
  last()	weight: 0
   nil()	weight: 0
 #app(x1,x2)	weight: 0
app❆1_tl(x1)	weight: 0
app❆1_reverse2(x1)	weight: 0
  cons()	weight: 0
app❆2_cons(x1,x2)	weight: (/ 1 2) + x1 + x2
#app❆1_hd(x1)	weight: 0
#app❆3_compose(x1,x2,x3)	weight: 0
app❆1_cons(x1)	weight: 0
#app❆1_reverse(x1)	weight: 0
   app(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #8
Number of SCCs: 1, DPs: 3, edges: 4
	SCC { #5 #6 #9 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#app❆2_reverse2(x1,x2)	weight: 0
    hd()	weight: 0
app❆1_reverse(x1)	weight: (/ 1 4)
app❆1_hd(x1)	weight: (/ 1 4)
  init()	weight: 0
#init()	weight: 0
app❆3_compose(x1,x2,x3)	weight: (/ 1 4) + x2
#app❆1_tl(x1)	weight: 0
reverse2()	weight: 0
app❆2_compose(x1,x2)	weight: (/ 1 4) + x1 + x2
reverse()	weight: 0
app❆2_reverse2(x1,x2)	weight: (/ 3 8) + x2
compose()	weight: 0
#last()	weight: 0
app❆1_compose(x1)	weight: (/ 1 4) + x1
    tl()	weight: 0
  last()	weight: 0
   nil()	weight: 0
 #app(x1,x2)	weight: x1
app❆1_tl(x1)	weight: (/ 1 4) + x1
app❆1_reverse2(x1)	weight: (/ 1 4) + x1
  cons()	weight: 0
app❆2_cons(x1,x2)	weight: (/ 1 4) + x1 + x2
#app❆1_hd(x1)	weight: 0
#app❆3_compose(x1,x2,x3)	weight: (/ 1 8) + x1 + x2
app❆1_cons(x1)	weight: (/ 1 4) + x1
#app❆1_reverse(x1)	weight: 0
   app(x1,x2)	weight: (/ 1 8)
    Usable rules: { }
    Removed DPs: #5 #6 #9
Number of SCCs: 0, DPs: 0, edges: 0
YES