MAYBE
Time: 0.000919
TRS:
 {      and(x, false()) -> false(),
    and(x, not false()) -> x,
              not not x -> x,
    implies(x, false()) -> not x,
    implies(false(), y) -> not false(),
  implies(not x, not y) -> implies(y, and(x, y))}
 DP:
  DP:
   {  implies#(x, false()) -> not# x,
      implies#(false(), y) -> not# false(),
    implies#(not x, not y) -> and#(x, y),
    implies#(not x, not y) -> implies#(y, and(x, y))}
  TRS:
  {      and(x, false()) -> false(),
     and(x, not false()) -> x,
               not not x -> x,
     implies(x, false()) -> not x,
     implies(false(), y) -> not false(),
   implies(not x, not y) -> implies(y, and(x, y))}
  EDG:
   {(implies#(not x, not y) -> implies#(y, and(x, y)), implies#(not x, not y) -> implies#(y, and(x, y)))
    (implies#(not x, not y) -> implies#(y, and(x, y)), implies#(not x, not y) -> and#(x, y))
    (implies#(not x, not y) -> implies#(y, and(x, y)), implies#(false(), y) -> not# false())
    (implies#(not x, not y) -> implies#(y, and(x, y)), implies#(x, false()) -> not# x)}
   STATUS:
    arrows: 0.750000
    SCCS (1):
     Scc:
      {implies#(not x, not y) -> implies#(y, and(x, y))}
     
     SCC (1):
      Strict:
       {implies#(not x, not y) -> implies#(y, and(x, y))}
      Weak:
      {      and(x, false()) -> false(),
         and(x, not false()) -> x,
                   not not x -> x,
         implies(x, false()) -> not x,
         implies(false(), y) -> not false(),
       implies(not x, not y) -> implies(y, and(x, y))}
      Open