MAYBE
Time: 0.053704
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))}
   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))}
      Open
     
     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))}
      Open