Input TRS:
    1: f(x,nil()) -> g(nil(),x)
    2: f(x,g(y,z)) -> g(f(x,y),z)
    3: ++(x,nil()) -> x
    4: ++(x,g(y,z)) -> g(++(x,y),z)
    5: null(nil()) -> true()
    6: null(g(x,y)) -> false()
    7: mem(nil(),y) -> false()
    8: mem(g(x,y),z) -> or(=(y,z),mem(x,z))
    9: mem(x,max(x)) -> not(null(x))
    10: max(g(g(nil(),x),y)) -> max'(x,y)
    11: max(g(g(g(x,y),z),u())) -> max'(max(g(g(x,y),z)),u())
Number of strict rules: 11
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #f(x,g(y,z)) -> #f(x,y)
   #2: #mem(x,max(x)) -> #null(x)
   #3: #max(g(g(g(x,y),z),u())) -> #max(g(g(x,y),z))
   #4: #mem(g(x,y),z) -> #mem(x,z)
   #5: #++(x,g(y,z)) -> #++(x,y)
Number of SCCs: 4, DPs: 4, edges: 4
	SCC { #5 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   mem(x1,x2)	weight: 0
  max'(x1,x2)	weight: 0
     u()	weight: 0
    ++(x1,x2)	weight: 0
 false()	weight: 0
 #mem(x1,x2)	weight: 0
  true()	weight: 0
     f(x1,x2)	weight: 0
  null(x1)	weight: 0
   max(x1)	weight: 0
     =(x1,x2)	weight: 0
  #++(x1,x2)	weight: x2
   nil()	weight: 0
 #max(x1)	weight: 0
    or(x1,x2)	weight: 0
   #f(x1,x2)	weight: 0
#null(x1)	weight: 0
     g(x1,x2)	weight: (/ 1 2) + x1
   not(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #5
Number of SCCs: 3, DPs: 3, edges: 3
	SCC { #1 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   mem(x1,x2)	weight: 0
  max'(x1,x2)	weight: 0
     u()	weight: 0
    ++(x1,x2)	weight: 0
 false()	weight: 0
 #mem(x1,x2)	weight: 0
  true()	weight: 0
     f(x1,x2)	weight: 0
  null(x1)	weight: 0
   max(x1)	weight: 0
     =(x1,x2)	weight: 0
  #++(x1,x2)	weight: 0
   nil()	weight: 0
 #max(x1)	weight: 0
    or(x1,x2)	weight: 0
   #f(x1,x2)	weight: x2
#null(x1)	weight: 0
     g(x1,x2)	weight: (/ 1 2) + x1
   not(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #1
Number of SCCs: 2, DPs: 2, edges: 2
	SCC { #4 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   mem(x1,x2)	weight: 0
  max'(x1,x2)	weight: 0
     u()	weight: 0
    ++(x1,x2)	weight: 0
 false()	weight: 0
 #mem(x1,x2)	weight: x1
  true()	weight: 0
     f(x1,x2)	weight: 0
  null(x1)	weight: 0
   max(x1)	weight: 0
     =(x1,x2)	weight: 0
  #++(x1,x2)	weight: 0
   nil()	weight: 0
 #max(x1)	weight: 0
    or(x1,x2)	weight: 0
   #f(x1,x2)	weight: 0
#null(x1)	weight: 0
     g(x1,x2)	weight: (/ 1 2) + x1
   not(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #4
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #3 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   mem(x1,x2)	weight: 0
  max'(x1,x2)	weight: 0
     u()	weight: 0
    ++(x1,x2)	weight: 0
 false()	weight: 0
 #mem(x1,x2)	weight: 0
  true()	weight: 0
     f(x1,x2)	weight: 0
  null(x1)	weight: 0
   max(x1)	weight: 0
     =(x1,x2)	weight: 0
  #++(x1,x2)	weight: 0
   nil()	weight: 0
 #max(x1)	weight: x1
    or(x1,x2)	weight: 0
   #f(x1,x2)	weight: 0
#null(x1)	weight: 0
     g(x1,x2)	weight: (/ 1 4) + x1 + x2
   not(x1)	weight: 0
    Usable rules: { }
    Removed DPs: #3
Number of SCCs: 0, DPs: 0, edges: 0
YES