MAYBE

Problem:
 and(x,false()) -> false()
 and(x,not(false())) -> x
 not(not(x)) -> x
 implies(false(),y) -> not(false())
 implies(x,false()) -> not(x)
 implies(not(x),not(y)) -> implies(y,and(x,y))

Proof:
 DP Processor:
  DPs:
   implies#(false(),y) -> not#(false())
   implies#(x,false()) -> not#(x)
   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(false(),y) -> not(false())
   implies(x,false()) -> not(x)
   implies(not(x),not(y)) -> implies(y,and(x,y))
  TDG Processor:
   DPs:
    implies#(false(),y) -> not#(false())
    implies#(x,false()) -> not#(x)
    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(false(),y) -> not(false())
    implies(x,false()) -> not(x)
    implies(not(x),not(y)) -> implies(y,and(x,y))
   graph:
    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#(x,false()) -> not#(x)
    implies#(not(x),not(y)) -> implies#(y,and(x,y)) -> implies#(false(),y) -> not#(false())
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 4/16
    DPs:
     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(false(),y) -> not(false())
     implies(x,false()) -> not(x)
     implies(not(x),not(y)) -> implies(y,and(x,y))
    Open