TRS:
 {       not(x) -> xor(x, true()),
  implies(x, y) -> xor(and(x, y), xor(x, true())),
       or(x, y) -> xor(and(x, y), xor(x, y)),
        =(x, y) -> xor(x, xor(y, true()))}
 RPO Product:
  Quasi-Precedence:
  empty
  
  Qed


TRS:
 {       not(x) -> xor(x, true()),
  implies(x, y) -> xor(and(x, y), xor(x, true())),
       or(x, y) -> xor(and(x, y), xor(x, y)),
        =(x, y) -> xor(x, xor(y, true()))}
 Cdiprover:
  Interpretation class: quasisimplemixed
  Complexity bound: POLYTIME COMPUTABLE IF RPO-TERMINATING
  =(X10, X9) = + 0*X10^2 + 0*X9^2 + 2*X10 + 2 + 2*X9 + 0*X9*X10
  or(X8, X7) = + 0*X8^2 + 0*X7^2 + 2*X8 + 3 + 2*X7 + 0*X7*X8
  implies(X6, X5) = + 0*X6^2 + 0*X5^2 + 2*X6 + 3 + 2*X5 + 0*X5*X6
  and(X4, X3) = + 1*X3 + 1*X4 + 1
  not(X2) = + 0*X2^2 + 2 + 2*X2
  true = + 0
  xor(X1, X0) = + 1*X0 + 1*X1 + 1
  
  Qed