MAYBE
Time: 0.003150
TRS:
 {        xor(x, x) -> F(),
        xor(x, F()) -> x,
      xor(x, neg x) -> F(),
              neg x -> xor(x, T()),
          and(x, x) -> x,
        and(x, F()) -> F(),
        and(x, T()) -> x,
  and(xor(x, y), z) -> xor(and(x, z), and(y, z)),
         impl(x, y) -> xor(and(x, y), xor(x, T())),
           or(x, y) -> xor(and(x, y), xor(x, y)),
        equiv(x, y) -> xor(x, xor(y, T()))}
 DP:
  DP:
   {            neg# x -> xor#(x, T()),
    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),
           impl#(x, y) -> xor#(x, T()),
           impl#(x, y) -> xor#(and(x, y), xor(x, T())),
           impl#(x, y) -> and#(x, y),
             or#(x, y) -> xor#(x, y),
             or#(x, y) -> xor#(and(x, y), xor(x, y)),
             or#(x, y) -> and#(x, y),
          equiv#(x, y) -> xor#(x, xor(y, T())),
          equiv#(x, y) -> xor#(y, T())}
  TRS:
  {        xor(x, x) -> F(),
         xor(x, F()) -> x,
       xor(x, neg x) -> F(),
               neg x -> xor(x, T()),
           and(x, x) -> x,
         and(x, F()) -> F(),
         and(x, T()) -> x,
   and(xor(x, y), z) -> xor(and(x, z), and(y, z)),
          impl(x, y) -> xor(and(x, y), xor(x, T())),
            or(x, y) -> xor(and(x, y), xor(x, y)),
         equiv(x, y) -> xor(x, xor(y, T()))}
  UR:
   {        xor(x, x) -> F(),
          xor(x, F()) -> x,
        xor(x, neg x) -> F(),
            and(x, x) -> x,
          and(x, F()) -> F(),
          and(x, T()) -> x,
    and(xor(x, y), z) -> xor(and(x, z), and(y, z)),
              a(w, v) -> w,
              a(w, v) -> v}
   EDG:
    {(or#(x, y) -> and#(x, y), and#(xor(x, y), 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) -> xor#(and(x, z), and(y, z)))
     (and#(xor(x, y), z) -> and#(y, z), and#(xor(x, y), 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) -> xor#(and(x, z), and(y, z)))
     (and#(xor(x, y), z) -> and#(x, z), 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#(x, z))
     (and#(xor(x, y), z) -> and#(x, z), and#(xor(x, y), z) -> and#(y, z))
     (impl#(x, y) -> and#(x, y), and#(xor(x, y), z) -> xor#(and(x, z), and(y, z)))
     (impl#(x, y) -> and#(x, y), and#(xor(x, y), z) -> and#(x, z))
     (impl#(x, y) -> and#(x, y), and#(xor(x, y), z) -> and#(y, z))}
    STATUS:
     arrows: 0.916667
     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) -> F(),
              xor(x, F()) -> x,
            xor(x, neg x) -> F(),
                    neg x -> xor(x, T()),
                and(x, x) -> x,
              and(x, F()) -> F(),
              and(x, T()) -> x,
        and(xor(x, y), z) -> xor(and(x, z), and(y, z)),
               impl(x, y) -> xor(and(x, y), xor(x, T())),
                 or(x, y) -> xor(and(x, y), xor(x, y)),
              equiv(x, y) -> xor(x, xor(y, T()))}
       Open