or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
↳ QTRS
↳ DependencyPairsProof
or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → AND(not(x), not(y))
NOT(or(x, y)) → NOT(y)
NOT(and(x, y)) → OR(not(x), not(y))
or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → AND(not(x), not(y))
NOT(or(x, y)) → NOT(y)
NOT(and(x, y)) → OR(not(x), not(y))
or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(y)
or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(y)
The value of delta used in the strict ordering is 8.
POL(NOT(x1)) = (4)x_1
POL(or(x1, x2)) = 4 + (4)x_1 + (4)x_2
POL(and(x1, x2)) = 2 + (4)x_1 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
or(x, x) → x
and(x, x) → x
not(not(x)) → x
not(and(x, y)) → or(not(x), not(y))
not(or(x, y)) → and(not(x), not(y))