MAYBE
Time: 0.001315
TRS:
 {        xor(x, x) -> false(),
    xor(x, false()) -> x,
              not x -> xor(x, true()),
          and(x, x) -> x,
     and(x, true()) -> x,
    and(x, false()) -> false(),
  and(xor(x, y), z) -> xor(and(x, z), and(y, z)),
           or(x, y) -> xor(and(x, y), xor(x, y)),
      implies(x, y) -> xor(and(x, y), xor(x, true()))}
 DP:
  DP:
   {            not# x -> xor#(x, true()),
    and#(xor(x, y), z) -> xor#(and(x, z), and(y, z)),
    and#(xor(x, y), z) -> and#(x, z),
    and#(xor(x, y), z) -> and#(y, z),
             or#(x, y) -> xor#(x, y),
             or#(x, y) -> xor#(and(x, y), xor(x, y)),
             or#(x, y) -> and#(x, y),
        implies#(x, y) -> xor#(x, true()),
        implies#(x, y) -> xor#(and(x, y), xor(x, true())),
        implies#(x, y) -> and#(x, y)}
  TRS:
  {        xor(x, x) -> false(),
     xor(x, false()) -> x,
               not x -> xor(x, true()),
           and(x, x) -> x,
      and(x, true()) -> x,
     and(x, false()) -> false(),
   and(xor(x, y), z) -> xor(and(x, z), and(y, z)),
            or(x, y) -> xor(and(x, y), xor(x, y)),
       implies(x, y) -> xor(and(x, y), xor(x, true()))}
  UR:
   {        xor(x, x) -> false(),
      xor(x, false()) -> x,
            and(x, x) -> x,
       and(x, true()) -> x,
      and(x, false()) -> false(),
    and(xor(x, y), z) -> xor(and(x, z), and(y, z)),
              a(w, v) -> w,
              a(w, v) -> v}
   EDG:
    {(and#(xor(x, y), z) -> and#(x, z), and#(xor(x, y), z) -> and#(y, z))
     (and#(xor(x, y), z) -> and#(x, z), and#(xor(x, y), z) -> and#(x, z))
     (and#(xor(x, y), z) -> and#(x, z), and#(xor(x, y), z) -> xor#(and(x, z), and(y, z)))
     (implies#(x, y) -> and#(x, y), and#(xor(x, y), z) -> and#(y, z))
     (implies#(x, y) -> and#(x, y), and#(xor(x, y), z) -> and#(x, z))
     (implies#(x, y) -> and#(x, y), and#(xor(x, y), z) -> xor#(and(x, z), and(y, z)))
     (or#(x, y) -> and#(x, y), and#(xor(x, y), z) -> xor#(and(x, z), and(y, z)))
     (or#(x, y) -> and#(x, y), and#(xor(x, y), z) -> and#(x, z))
     (or#(x, y) -> and#(x, y), and#(xor(x, y), z) -> and#(y, z))
     (and#(xor(x, y), z) -> and#(y, z), and#(xor(x, y), z) -> xor#(and(x, z), and(y, z)))
     (and#(xor(x, y), z) -> and#(y, z), and#(xor(x, y), z) -> and#(x, z))
     (and#(xor(x, y), z) -> and#(y, z), and#(xor(x, y), z) -> and#(y, z))}
    STATUS:
     arrows: 0.880000
     SCCS (1):
      Scc:
       {and#(xor(x, y), z) -> and#(x, z),
        and#(xor(x, y), z) -> and#(y, z)}
      
      
      
      
      
      
      SCC (2):
       Strict:
        {and#(xor(x, y), z) -> and#(x, z),
         and#(xor(x, y), z) -> and#(y, z)}
       Weak:
       {        xor(x, x) -> false(),
          xor(x, false()) -> x,
                    not x -> xor(x, true()),
                and(x, x) -> x,
           and(x, true()) -> x,
          and(x, false()) -> false(),
        and(xor(x, y), z) -> xor(and(x, z), and(y, z)),
                 or(x, y) -> xor(and(x, y), xor(x, y)),
            implies(x, y) -> xor(and(x, y), xor(x, true()))}
       Open