MAYBE
Time: 0.001646
TRS:
 {               or(x, x) -> x,
          or(x, or(y, y)) -> or(x, y),
         or(x, and(x, y)) -> x,
           or(x, false()) -> x,
  or(or(x, y), and(y, z)) -> or(x, y),
            or(true(), y) -> true(),
                and(x, x) -> x,
         and(x, or(y, z)) -> or(and(x, y), and(x, z)),
        and(x, and(y, y)) -> and(x, y),
           and(x, true()) -> x,
          and(false(), y) -> false()}
 DP:
  DP:
   {  or#(x, or(y, y)) -> or#(x, y),
     and#(x, or(y, z)) -> or#(and(x, y), and(x, z)),
     and#(x, or(y, z)) -> and#(x, y),
     and#(x, or(y, z)) -> and#(x, z),
    and#(x, and(y, y)) -> and#(x, y)}
  TRS:
  {               or(x, x) -> x,
           or(x, or(y, y)) -> or(x, y),
          or(x, and(x, y)) -> x,
            or(x, false()) -> x,
   or(or(x, y), and(y, z)) -> or(x, y),
             or(true(), y) -> true(),
                 and(x, x) -> x,
          and(x, or(y, z)) -> or(and(x, y), and(x, z)),
         and(x, and(y, y)) -> and(x, y),
            and(x, true()) -> x,
           and(false(), y) -> false()}
  UR:
   {               or(x, x) -> x,
            or(x, or(y, y)) -> or(x, y),
           or(x, and(x, y)) -> x,
             or(x, false()) -> x,
    or(or(x, y), and(y, z)) -> or(x, y),
              or(true(), y) -> true(),
                  and(x, x) -> x,
           and(x, or(y, z)) -> or(and(x, y), and(x, z)),
          and(x, and(y, y)) -> and(x, y),
             and(x, true()) -> x,
            and(false(), y) -> false(),
                    a(w, v) -> w,
                    a(w, v) -> v}
   EDG:
    {(and#(x, or(y, z)) -> and#(x, y), and#(x, and(y, y)) -> 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#(x, or(y, z)) -> and#(x, y))
     (and#(x, or(y, z)) -> and#(x, y), and#(x, or(y, z)) -> or#(and(x, y), and(x, z)))
     (and#(x, or(y, z)) -> or#(and(x, y), and(x, z)), or#(x, or(y, y)) -> or#(x, y))
     (and#(x, or(y, z)) -> and#(x, z), and#(x, or(y, z)) -> or#(and(x, y), 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#(x, and(y, y)) -> and#(x, y))
     (and#(x, and(y, y)) -> and#(x, y), and#(x, or(y, z)) -> or#(and(x, y), and(x, z)))
     (and#(x, and(y, y)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, y))
     (and#(x, and(y, y)) -> and#(x, y), and#(x, or(y, z)) -> and#(x, z))
     (and#(x, and(y, y)) -> and#(x, y), and#(x, and(y, y)) -> and#(x, y))
     (or#(x, or(y, y)) -> or#(x, y), or#(x, or(y, y)) -> or#(x, y))}
    STATUS:
     arrows: 0.440000
     SCCS (2):
      Scc:
       { and#(x, or(y, z)) -> and#(x, y),
         and#(x, or(y, z)) -> and#(x, z),
        and#(x, and(y, y)) -> and#(x, y)}
      Scc:
       {or#(x, or(y, y)) -> or#(x, y)}
      
      SCC (3):
       Strict:
        { and#(x, or(y, z)) -> and#(x, y),
          and#(x, or(y, z)) -> and#(x, z),
         and#(x, and(y, y)) -> and#(x, y)}
       Weak:
       {               or(x, x) -> x,
                or(x, or(y, y)) -> or(x, y),
               or(x, and(x, y)) -> x,
                 or(x, false()) -> x,
        or(or(x, y), and(y, z)) -> or(x, y),
                  or(true(), y) -> true(),
                      and(x, x) -> x,
               and(x, or(y, z)) -> or(and(x, y), and(x, z)),
              and(x, and(y, y)) -> and(x, y),
                 and(x, true()) -> x,
                and(false(), y) -> false()}
       Open
      
      SCC (1):
       Strict:
        {or#(x, or(y, y)) -> or#(x, y)}
       Weak:
       {               or(x, x) -> x,
                or(x, or(y, y)) -> or(x, y),
               or(x, and(x, y)) -> x,
                 or(x, false()) -> x,
        or(or(x, y), and(y, z)) -> or(x, y),
                  or(true(), y) -> true(),
                      and(x, x) -> x,
               and(x, or(y, z)) -> or(and(x, y), and(x, z)),
              and(x, and(y, y)) -> and(x, y),
                 and(x, true()) -> x,
                and(false(), y) -> false()}
       Open