YES Time: 0.031356 TRS: { not not x -> x, not and(x, y) -> or(not not not x, not not not y), not or(x, y) -> and(not not not x, not not not y)} DP: DP: {not# and(x, y) -> not# x, not# and(x, y) -> not# y, not# and(x, y) -> not# not x, not# and(x, y) -> not# not y, not# and(x, y) -> not# not not x, not# and(x, y) -> not# not not y, not# or(x, y) -> not# x, not# or(x, y) -> not# y, not# or(x, y) -> not# not x, not# or(x, y) -> not# not y, not# or(x, y) -> not# not not x, not# or(x, y) -> not# not not y} TRS: { not not x -> x, not and(x, y) -> or(not not not x, not not not y), not or(x, y) -> and(not not not x, not not not y)} UR: { not not x -> x, not and(x, y) -> or(not not not x, not not not y), not or(x, y) -> and(not not not x, not not not y)} EDG: {(not# and(x, y) -> not# not not y, not# or(x, y) -> not# not not y) (not# and(x, y) -> not# not not y, not# or(x, y) -> not# not not x) (not# and(x, y) -> not# not not y, not# or(x, y) -> not# not y) (not# and(x, y) -> not# not not y, not# or(x, y) -> not# not x) (not# and(x, y) -> not# not not y, not# or(x, y) -> not# y) (not# and(x, y) -> not# not not y, not# or(x, y) -> not# x) (not# and(x, y) -> not# not not y, not# and(x, y) -> not# not not y) (not# and(x, y) -> not# not not y, not# and(x, y) -> not# not not x) (not# and(x, y) -> not# not not y, not# and(x, y) -> not# not y) (not# and(x, y) -> not# not not y, not# and(x, y) -> not# not x) (not# and(x, y) -> not# not not y, not# and(x, y) -> not# y) (not# and(x, y) -> not# not not y, not# and(x, y) -> not# x) (not# or(x, y) -> not# not not y, not# or(x, y) -> not# not not y) (not# or(x, y) -> not# not not y, not# or(x, y) -> not# not not x) (not# or(x, y) -> not# not not y, not# or(x, y) -> not# not y) (not# or(x, y) -> not# not not y, not# or(x, y) -> not# not x) (not# or(x, y) -> not# not not y, not# or(x, y) -> not# y) (not# or(x, y) -> not# not not y, not# or(x, y) -> not# x) (not# or(x, y) -> not# not not y, not# and(x, y) -> not# not not y) (not# or(x, y) -> not# not not y, not# and(x, y) -> not# not not x) (not# or(x, y) -> not# not not y, not# and(x, y) -> not# not y) (not# or(x, y) -> not# not not y, not# and(x, y) -> not# not x) (not# or(x, y) -> not# not not y, not# and(x, y) -> not# y) (not# or(x, y) -> not# not not y, not# and(x, y) -> not# x) (not# or(x, y) -> not# y, not# or(x, y) -> not# not not y) (not# or(x, y) -> not# y, not# or(x, y) -> not# not not x) (not# or(x, y) -> not# y, not# or(x, y) -> not# not y) (not# or(x, y) -> not# y, not# or(x, y) -> not# not x) (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# not not y) (not# or(x, y) -> not# y, not# and(x, y) -> not# not not x) (not# or(x, y) -> not# y, not# and(x, y) -> not# not y) (not# or(x, y) -> not# y, not# and(x, y) -> not# 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) -> not# x, not# or(x, y) -> not# not not y) (not# or(x, y) -> not# x, not# or(x, y) -> not# not not x) (not# or(x, y) -> not# x, not# or(x, y) -> not# not y) (not# or(x, y) -> not# x, not# or(x, y) -> not# not x) (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# not not y) (not# or(x, y) -> not# x, not# and(x, y) -> not# not not x) (not# or(x, y) -> not# x, not# and(x, y) -> not# not y) (not# or(x, y) -> not# x, not# and(x, y) -> not# 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) (not# or(x, y) -> not# not y, not# or(x, y) -> not# not not y) (not# or(x, y) -> not# not y, not# or(x, y) -> not# not not x) (not# or(x, y) -> not# not y, not# or(x, y) -> not# not y) (not# or(x, y) -> not# not y, not# or(x, y) -> not# not x) (not# or(x, y) -> not# not y, not# or(x, y) -> not# y) (not# or(x, y) -> not# not y, not# or(x, y) -> not# x) (not# or(x, y) -> not# not y, not# and(x, y) -> not# not not y) (not# or(x, y) -> not# not y, not# and(x, y) -> not# not not x) (not# or(x, y) -> not# not y, not# and(x, y) -> not# not y) (not# or(x, y) -> not# not y, not# and(x, y) -> not# not x) (not# or(x, y) -> not# not y, not# and(x, y) -> not# y) (not# or(x, y) -> not# not y, not# and(x, y) -> not# x) (not# or(x, y) -> not# not x, not# or(x, y) -> not# not not y) (not# or(x, y) -> not# not x, not# or(x, y) -> not# not not x) (not# or(x, y) -> not# not x, not# or(x, y) -> not# not y) (not# or(x, y) -> not# not x, not# or(x, y) -> not# not x) (not# or(x, y) -> not# not x, not# or(x, y) -> not# y) (not# or(x, y) -> not# not x, not# or(x, y) -> not# x) (not# or(x, y) -> not# not x, not# and(x, y) -> not# not not y) (not# or(x, y) -> not# not x, not# and(x, y) -> not# not not x) (not# or(x, y) -> not# not x, not# and(x, y) -> not# not y) (not# or(x, y) -> not# not x, not# and(x, y) -> not# not x) (not# or(x, y) -> not# not x, not# and(x, y) -> not# y) (not# or(x, y) -> not# not x, not# and(x, y) -> not# x) (not# and(x, y) -> not# not x, not# and(x, y) -> not# x) (not# and(x, y) -> not# not x, not# and(x, y) -> not# y) (not# and(x, y) -> not# not x, not# and(x, y) -> not# not x) (not# and(x, y) -> not# not x, not# and(x, y) -> not# not y) (not# and(x, y) -> not# not x, not# and(x, y) -> not# not not x) (not# and(x, y) -> not# not x, not# and(x, y) -> not# not not y) (not# and(x, y) -> not# not x, not# or(x, y) -> not# x) (not# and(x, y) -> not# not x, not# or(x, y) -> not# y) (not# and(x, y) -> not# not x, not# or(x, y) -> not# not x) (not# and(x, y) -> not# not x, not# or(x, y) -> not# not y) (not# and(x, y) -> not# not x, not# or(x, y) -> not# not not x) (not# and(x, y) -> not# not x, not# or(x, y) -> not# not not y) (not# and(x, y) -> not# not y, not# and(x, y) -> not# x) (not# and(x, y) -> not# not y, not# and(x, y) -> not# y) (not# and(x, y) -> not# not y, not# and(x, y) -> not# not x) (not# and(x, y) -> not# not y, not# and(x, y) -> not# not y) (not# and(x, y) -> not# not y, not# and(x, y) -> not# not not x) (not# and(x, y) -> not# not y, not# and(x, y) -> not# not not y) (not# and(x, y) -> not# not y, not# or(x, y) -> not# x) (not# and(x, y) -> not# not y, not# or(x, y) -> not# y) (not# and(x, y) -> not# not y, not# or(x, y) -> not# not x) (not# and(x, y) -> not# not y, not# or(x, y) -> not# not y) (not# and(x, y) -> not# not y, not# or(x, y) -> not# not not x) (not# and(x, y) -> not# not y, not# or(x, y) -> not# not 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# and(x, y) -> not# not x) (not# and(x, y) -> not# x, not# and(x, y) -> not# not y) (not# and(x, y) -> not# x, not# and(x, y) -> not# not not x) (not# and(x, y) -> not# x, not# and(x, y) -> not# not 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) -> not# not x) (not# and(x, y) -> not# x, not# or(x, y) -> not# not y) (not# and(x, y) -> not# x, not# or(x, y) -> not# not not x) (not# and(x, y) -> not# x, not# or(x, y) -> not# not not y) (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# and(x, y) -> not# not x) (not# and(x, y) -> not# y, not# and(x, y) -> not# not y) (not# and(x, y) -> not# y, not# and(x, y) -> not# not not x) (not# and(x, y) -> not# y, not# and(x, y) -> not# not 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) -> not# not x) (not# and(x, y) -> not# y, not# or(x, y) -> not# not y) (not# and(x, y) -> not# y, not# or(x, y) -> not# not not x) (not# and(x, y) -> not# y, not# or(x, y) -> not# not not y) (not# or(x, y) -> not# not not x, not# and(x, y) -> not# x) (not# or(x, y) -> not# not not x, not# and(x, y) -> not# y) (not# or(x, y) -> not# not not x, not# and(x, y) -> not# not x) (not# or(x, y) -> not# not not x, not# and(x, y) -> not# not y) (not# or(x, y) -> not# not not x, not# and(x, y) -> not# not not x) (not# or(x, y) -> not# not not x, not# and(x, y) -> not# not not y) (not# or(x, y) -> not# not not x, not# or(x, y) -> not# x) (not# or(x, y) -> not# not not x, not# or(x, y) -> not# y) (not# or(x, y) -> not# not not x, not# or(x, y) -> not# not x) (not# or(x, y) -> not# not not x, not# or(x, y) -> not# not y) (not# or(x, y) -> not# not not x, not# or(x, y) -> not# not not x) (not# or(x, y) -> not# not not x, not# or(x, y) -> not# not not y) (not# and(x, y) -> not# not not x, not# and(x, y) -> not# x) (not# and(x, y) -> not# not not x, not# and(x, y) -> not# y) (not# and(x, y) -> not# not not x, not# and(x, y) -> not# not x) (not# and(x, y) -> not# not not x, not# and(x, y) -> not# not y) (not# and(x, y) -> not# not not x, not# and(x, y) -> not# not not x) (not# and(x, y) -> not# not not x, not# and(x, y) -> not# not not y) (not# and(x, y) -> not# not not x, not# or(x, y) -> not# x) (not# and(x, y) -> not# not not x, not# or(x, y) -> not# y) (not# and(x, y) -> not# not not x, not# or(x, y) -> not# not x) (not# and(x, y) -> not# not not x, not# or(x, y) -> not# not y) (not# and(x, y) -> not# not not x, not# or(x, y) -> not# not not x) (not# and(x, y) -> not# not not x, not# or(x, y) -> not# not not y)} STATUS: arrows: 0.000000 SCCS (1): Scc: {not# and(x, y) -> not# x, not# and(x, y) -> not# y, not# and(x, y) -> not# not x, not# and(x, y) -> not# not y, not# and(x, y) -> not# not not x, not# and(x, y) -> not# not not y, not# or(x, y) -> not# x, not# or(x, y) -> not# y, not# or(x, y) -> not# not x, not# or(x, y) -> not# not y, not# or(x, y) -> not# not not x, not# or(x, y) -> not# not not y} SCC (12): Strict: {not# and(x, y) -> not# x, not# and(x, y) -> not# y, not# and(x, y) -> not# not x, not# and(x, y) -> not# not y, not# and(x, y) -> not# not not x, not# and(x, y) -> not# not not y, not# or(x, y) -> not# x, not# or(x, y) -> not# y, not# or(x, y) -> not# not x, not# or(x, y) -> not# not y, not# or(x, y) -> not# not not x, not# or(x, y) -> not# not not y} Weak: { not not x -> x, not and(x, y) -> or(not not not x, not not not y), not or(x, y) -> and(not not not x, not not not y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [and](x0, x1) = x0 + x1 + 1, [or](x0, x1) = x0 + x1 + 1, [not](x0) = x0, [not#](x0) = x0 Strict: not# or(x, y) -> not# not not y 1 + 1x + 1y >= 0 + 1y not# or(x, y) -> not# not not x 1 + 1x + 1y >= 0 + 1x not# or(x, y) -> not# not y 1 + 1x + 1y >= 0 + 1y not# or(x, y) -> not# not x 1 + 1x + 1y >= 0 + 1x 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# not not y 1 + 1x + 1y >= 0 + 1y not# and(x, y) -> not# not not x 1 + 1x + 1y >= 0 + 1x not# and(x, y) -> not# not y 1 + 1x + 1y >= 0 + 1y not# and(x, y) -> not# not x 1 + 1x + 1y >= 0 + 1x not# and(x, y) -> not# y 1 + 1x + 1y >= 0 + 1y not# and(x, y) -> not# x 1 + 1x + 1y >= 0 + 1x Weak: not or(x, y) -> and(not not not x, not not not y) 1 + 1x + 1y >= 1 + 1x + 1y not and(x, y) -> or(not not not x, not not not y) 1 + 1x + 1y >= 1 + 1x + 1y not not x -> x 0 + 1x >= 1x Qed