YES Time: 0.018787 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))} UR: { 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)), a(w, v) -> w, a(w, v) -> v} 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))} STATUS: arrows: 0.506173 SCCS (2): 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: {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 (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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [and](x0, x1) = x0 + x1, [or](x0, x1) = x0 + x1 + 1, [not](x0) = x0 + 1, [not#](x0) = x0 Strict: not# or(x, y) -> not# y 1 + 1x + 1y >= 0 + 1y not# or(x, y) -> not# x 1 + 1x + 1y >= 0 + 1x not# and(x, y) -> not# y 0 + 1x + 1y >= 0 + 1y not# and(x, y) -> not# x 0 + 1x + 1y >= 0 + 1x Weak: and(or(y, z), x) -> or(and(x, y), and(x, z)) 1 + 1x + 1y + 1z >= 1 + 2x + 1y + 1z and(x, or(y, z)) -> or(and(x, y), and(x, z)) 1 + 1x + 1y + 1z >= 1 + 2x + 1y + 1z not or(x, y) -> and(not x, not y) 2 + 1x + 1y >= 2 + 1x + 1y not and(x, y) -> or(not x, not y) 1 + 1x + 1y >= 3 + 1x + 1y not not x -> x 2 + 1x >= 1x SCCS (1): Scc: {not# and(x, y) -> not# x, not# and(x, y) -> not# y} SCC (2): Strict: {not# and(x, y) -> not# x, not# and(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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [and](x0, x1) = x0 + x1 + 1, [or](x0, x1) = 0, [not](x0) = x0 + 1, [not#](x0) = x0 Strict: not# and(x, y) -> not# y 1 + 1x + 1y >= 0 + 1y not# and(x, y) -> not# x 1 + 1x + 1y >= 0 + 1x Weak: and(or(y, z), x) -> or(and(x, y), and(x, z)) 1 + 1x + 0y + 0z >= 0 + 0x + 0y + 0z and(x, or(y, z)) -> or(and(x, y), and(x, z)) 1 + 1x + 0y + 0z >= 0 + 0x + 0y + 0z not or(x, y) -> and(not x, not y) 1 + 0x + 0y >= 3 + 1x + 1y not and(x, y) -> or(not x, not y) 2 + 1x + 1y >= 0 + 0x + 0y not not x -> x 2 + 1x >= 1x Qed 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: and(or(y, z), x) -> or(and(x, y), and(x, z)) 1 + 0x + 0y + 0z >= 3 + 0x + 0y + 0z and(x, or(y, z)) -> or(and(x, y), and(x, z)) 1 + 0x + 0y + 0z >= 3 + 0x + 0y + 0z not or(x, y) -> and(not x, not y) 2 + 1x + 1y >= 1 + 0x + 0y not and(x, y) -> or(not x, not y) 2 + 0x + 0y >= 3 + 1x + 1y not not x -> x 2 + 1x >= 1x Qed