YES Time: 0.008306 TRS: { not not x -> x, not and(x, y) -> or(not x, not y), not or(x, y) -> and(not x, not y), and(x, or(y, z)) -> or(and(x, y), and(x, z)), and(or(y, z), x) -> or(and(x, y), and(x, z))} DP: DP: { not# and(x, y) -> not# x, not# and(x, y) -> not# y, not# or(x, y) -> not# x, not# or(x, y) -> not# y, not# or(x, y) -> and#(not x, not y), and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, z), and#(or(y, z), x) -> and#(x, y), and#(or(y, z), x) -> and#(x, z)} TRS: { not not x -> x, not and(x, y) -> or(not x, not y), not or(x, y) -> and(not x, not y), and(x, or(y, z)) -> or(and(x, y), and(x, z)), and(or(y, z), x) -> or(and(x, y), and(x, z))} EDG: {(not# or(x, y) -> not# x, not# or(x, y) -> and#(not x, not y)) (not# or(x, y) -> not# x, not# or(x, y) -> not# y) (not# or(x, y) -> not# x, not# or(x, y) -> not# x) (not# or(x, y) -> not# x, not# and(x, y) -> not# y) (not# or(x, y) -> not# x, not# and(x, y) -> not# x) (and#(or(y, z), x) -> and#(x, z), and#(or(y, z), x) -> and#(x, z)) (and#(or(y, z), x) -> and#(x, z), and#(or(y, z), x) -> and#(x, y)) (and#(or(y, z), x) -> and#(x, z), and#(x, or(y, z)) -> and#(x, z)) (and#(or(y, z), x) -> and#(x, z), and#(x, or(y, z)) -> and#(x, y)) (and#(or(y, z), x) -> and#(x, y), and#(or(y, z), x) -> and#(x, z)) (and#(or(y, z), x) -> and#(x, y), and#(or(y, z), x) -> and#(x, y)) (and#(or(y, z), x) -> and#(x, y), and#(x, or(y, z)) -> and#(x, z)) (and#(or(y, z), x) -> and#(x, y), and#(x, or(y, z)) -> and#(x, y)) (not# or(x, y) -> not# y, not# or(x, y) -> and#(not x, not y)) (not# or(x, y) -> not# y, not# or(x, y) -> not# y) (not# or(x, y) -> not# y, not# or(x, y) -> not# x) (not# or(x, y) -> not# y, not# and(x, y) -> not# y) (not# or(x, y) -> not# y, not# and(x, y) -> not# x) (not# or(x, y) -> and#(not x, not y), and#(x, or(y, z)) -> and#(x, y)) (not# or(x, y) -> and#(not x, not y), and#(x, or(y, z)) -> and#(x, z)) (not# or(x, y) -> and#(not x, not y), and#(or(y, z), x) -> and#(x, y)) (not# or(x, y) -> and#(not x, not y), and#(or(y, z), x) -> and#(x, z)) (not# and(x, y) -> not# y, not# and(x, y) -> not# x) (not# and(x, y) -> not# y, not# and(x, y) -> not# y) (not# and(x, y) -> not# y, not# or(x, y) -> not# x) (not# and(x, y) -> not# y, not# or(x, y) -> not# y) (not# and(x, y) -> not# y, not# or(x, y) -> and#(not x, not y)) (and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, y)) (and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, z)) (and#(x, or(y, z)) -> and#(x, y), and#(or(y, z), x) -> and#(x, y)) (and#(x, or(y, z)) -> and#(x, y), and#(or(y, z), x) -> and#(x, z)) (and#(x, or(y, z)) -> and#(x, z), and#(x, or(y, z)) -> and#(x, y)) (and#(x, or(y, z)) -> and#(x, z), and#(x, or(y, z)) -> and#(x, z)) (and#(x, or(y, z)) -> and#(x, z), and#(or(y, z), x) -> and#(x, y)) (and#(x, or(y, z)) -> and#(x, z), and#(or(y, z), x) -> and#(x, z)) (not# and(x, y) -> not# x, not# and(x, y) -> not# x) (not# and(x, y) -> not# x, not# and(x, y) -> not# y) (not# and(x, y) -> not# x, not# or(x, y) -> not# x) (not# and(x, y) -> not# x, not# or(x, y) -> not# y) (not# and(x, y) -> not# x, not# or(x, y) -> and#(not x, not y))} SCCS (2): Scc: {and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, z), and#(or(y, z), x) -> and#(x, y), and#(or(y, z), x) -> and#(x, z)} Scc: {not# and(x, y) -> not# x, not# and(x, y) -> not# y, not# or(x, y) -> not# x, not# or(x, y) -> not# y} SCC (4): Strict: {and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, z), and#(or(y, z), x) -> and#(x, y), and#(or(y, z), x) -> and#(x, z)} Weak: { not not x -> x, not and(x, y) -> or(not x, not y), not or(x, y) -> and(not x, not y), and(x, or(y, z)) -> or(and(x, y), and(x, z)), and(or(y, z), x) -> or(and(x, y), and(x, z))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [and](x0, x1) = 1, [or](x0, x1) = x0 + x1 + 1, [not](x0) = x0 + 1, [and#](x0, x1) = x0 + x1 Strict: and#(or(y, z), x) -> and#(x, z) 1 + 1x + 1y + 1z >= 0 + 1x + 1z and#(or(y, z), x) -> and#(x, y) 1 + 1x + 1y + 1z >= 0 + 1x + 1y and#(x, or(y, z)) -> and#(x, z) 1 + 1x + 1y + 1z >= 0 + 1x + 1z and#(x, or(y, z)) -> and#(x, y) 1 + 1x + 1y + 1z >= 0 + 1x + 1y Weak: Qed SCC (4): Strict: {not# and(x, y) -> not# x, not# and(x, y) -> not# y, not# or(x, y) -> not# x, not# or(x, y) -> not# y} Weak: { not not x -> x, not and(x, y) -> or(not x, not y), not or(x, y) -> and(not x, not y), and(x, or(y, z)) -> or(and(x, y), and(x, z)), and(or(y, z), x) -> or(and(x, y), and(x, z))} SPSC: Simple Projection: pi(not#) = 0 Strict: {not# and(x, y) -> not# x, not# and(x, y) -> not# y, not# or(x, y) -> not# y} EDG: {(not# and(x, y) -> not# y, not# or(x, y) -> not# y) (not# and(x, y) -> not# y, not# and(x, y) -> not# y) (not# and(x, y) -> not# y, not# and(x, y) -> not# x) (not# or(x, y) -> not# y, not# and(x, y) -> not# x) (not# or(x, y) -> not# y, not# and(x, y) -> not# y) (not# or(x, y) -> not# y, not# or(x, y) -> not# y) (not# and(x, y) -> not# x, not# and(x, y) -> not# x) (not# and(x, y) -> not# x, not# and(x, y) -> not# y) (not# and(x, y) -> not# x, not# or(x, y) -> not# y)} SCCS (1): Scc: {not# and(x, y) -> not# x, not# and(x, y) -> not# y, not# or(x, y) -> not# y} SCC (3): Strict: {not# and(x, y) -> not# x, not# and(x, y) -> not# y, not# or(x, y) -> not# y} Weak: { not not x -> x, not and(x, y) -> or(not x, not y), not or(x, y) -> and(not x, not y), and(x, or(y, z)) -> or(and(x, y), and(x, z)), and(or(y, z), x) -> or(and(x, y), and(x, z))} SPSC: Simple Projection: pi(not#) = 0 Strict: {not# and(x, y) -> not# x, not# or(x, y) -> not# y} EDG: {(not# or(x, y) -> not# y, not# or(x, y) -> not# y) (not# or(x, y) -> not# y, not# and(x, y) -> not# x) (not# and(x, y) -> not# x, not# and(x, y) -> not# x) (not# and(x, y) -> not# x, not# or(x, y) -> not# y)} SCCS (1): Scc: {not# and(x, y) -> not# x, not# or(x, y) -> not# y} SCC (2): Strict: {not# and(x, y) -> not# x, not# or(x, y) -> not# y} Weak: { not not x -> x, not and(x, y) -> or(not x, not y), not or(x, y) -> and(not x, not y), and(x, or(y, z)) -> or(and(x, y), and(x, z)), and(or(y, z), x) -> or(and(x, y), and(x, z))} SPSC: Simple Projection: pi(not#) = 0 Strict: {not# or(x, y) -> not# y} EDG: {(not# or(x, y) -> not# y, not# or(x, y) -> not# y)} SCCS (1): Scc: {not# or(x, y) -> not# y} SCC (1): Strict: {not# or(x, y) -> not# y} Weak: { not not x -> x, not and(x, y) -> or(not x, not y), not or(x, y) -> and(not x, not y), and(x, or(y, z)) -> or(and(x, y), and(x, z)), and(or(y, z), x) -> or(and(x, y), and(x, z))} SPSC: Simple Projection: pi(not#) = 0 Strict: {} Qed