Input TRS:
    1: rev1(0(),nil()) -> 0()
    2: rev1(s(X),nil()) -> s(X)
    3: rev1(X,cons(Y,L)) -> rev1(Y,L)
    4: rev(nil()) -> nil()
    5: rev(cons(X,L)) -> cons(rev1(X,L),rev2(X,L))
    6: rev2(X,nil()) -> nil()
    7: rev2(X,cons(Y,L)) -> rev(cons(X,rev(rev2(Y,L))))
Number of strict rules: 7
Direct Order(PosReal,>,Poly) ... failed.
Freezing rev
1: rev1(0(),nil()) -> 0()
2: rev1(s(X),nil()) -> s(X)
3: rev1(X,cons(Y,L)) -> rev1(Y,L)
4: rev❆1_nil() -> nil()
5: rev❆1_cons(X,L) -> cons(rev1(X,L),rev2(X,L))
6: rev2(X,nil()) -> nil()
7: rev2(X,cons(Y,L)) -> rev❆1_cons(X,rev(rev2(Y,L)))
8: rev(cons(_1,_2)) ->= rev❆1_cons(_1,_2)
9: rev(nil()) ->= rev❆1_nil()
Number of strict rules: 7
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #rev(nil()) ->? #rev❆1_nil()
   #2: #rev2(X,cons(Y,L)) -> #rev❆1_cons(X,rev(rev2(Y,L)))
   #3: #rev2(X,cons(Y,L)) -> #rev(rev2(Y,L))
   #4: #rev2(X,cons(Y,L)) -> #rev2(Y,L)
   #5: #rev❆1_cons(X,L) -> #rev1(X,L)
   #6: #rev❆1_cons(X,L) -> #rev2(X,L)
   #7: #rev1(X,cons(Y,L)) -> #rev1(Y,L)
   #8: #rev(cons(_1,_2)) ->? #rev❆1_cons(_1,_2)
Number of SCCs: 2, DPs: 6, edges: 10
	SCC { #7 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #rev(x1)	weight: 0
     s(x1)	weight: 0
  rev1(x1,x2)	weight: 0
rev❆1_nil()	weight: 0
#rev1(x1,x2)	weight: x2
#rev2(x1,x2)	weight: 0
     0()	weight: 0
rev❆1_cons(x1,x2)	weight: 0
   nil()	weight: 0
   rev(x1)	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x2
#rev❆1_cons(x1,x2)	weight: 0
  rev2(x1,x2)	weight: 0
#rev❆1_nil()	weight: 0
    Usable rules: { }
    Removed DPs: #7
Number of SCCs: 1, DPs: 5, edges: 9
	SCC { #2..4 #6 #8 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
 #rev(x1)	weight: (/ 1 4) + x1
     s(x1)	weight: (/ 1 2) + x1
  rev1(x1,x2)	weight: (/ 1 4)
rev❆1_nil()	weight: 0
#rev1(x1,x2)	weight: 0
#rev2(x1,x2)	weight: x2
     0()	weight: 0
rev❆1_cons(x1,x2)	weight: (/ 1 2) + x2
   nil()	weight: 0
   rev(x1)	weight: x1
  cons(x1,x2)	weight: (/ 1 2) + x2
#rev❆1_cons(x1,x2)	weight: (/ 1 4) + x2
  rev2(x1,x2)	weight: x2
#rev❆1_nil()	weight: 0
    Usable rules: { 4..9 }
    Removed DPs: #2..4 #6 #8
Number of SCCs: 0, DPs: 0, edges: 0
YES