TRS:
 {       or(true(), y) -> true(),
         or(x, true()) -> true(),
  or(false(), false()) -> false(),
         mem(x, nil()) -> false(),
        mem(x, set(y)) -> =(x, y),
   mem(x, union(y, z)) -> or(mem(x, y), mem(x, z))}
 RPO Product:
  Quasi-Precedence:
  mem > or
  empty
  
  Qed


TRS:
 {       or(true(), y) -> true(),
         or(x, true()) -> true(),
  or(false(), false()) -> false(),
         mem(x, nil()) -> false(),
        mem(x, set(y)) -> =(x, y),
   mem(x, union(y, z)) -> or(mem(x, y), mem(x, z))}
 Cdiprover:
  Interpretation class: quasisimplemixed
  Complexity bound: POLYTIME COMPUTABLE IF RPO-TERMINATING
  union(X8, X7) = + 1*X7 + 1*X8 + 1
  set(X6) = + 1*X6 + 2
  =(X5, X4) = + 1*X4 + 1*X5 + 4
  nil = + 0
  mem(X3, X2) = + 0*X3^2 + 0*X2^2 + 1*X3 + 0 + 2*X2 + 3*X2*X3
  false = + 0
  or(X1, X0) = + 0*X1^2 + 0*X0^2 + 1*X1 + 2 + 1*X0 + 0*X0*X1
  true = + 0
  
  Qed