MAYBE

Problem:
 not(not(x)) -> x
 not(or(x,y)) -> and(not(not(not(x))),not(not(not(y))))
 not(and(x,y)) -> or(not(not(not(x))),not(not(not(y))))

Proof:
 DP Processor:
  DPs:
   not#(or(x,y)) -> not#(y)
   not#(or(x,y)) -> not#(not(y))
   not#(or(x,y)) -> not#(not(not(y)))
   not#(or(x,y)) -> not#(x)
   not#(or(x,y)) -> not#(not(x))
   not#(or(x,y)) -> not#(not(not(x)))
   not#(and(x,y)) -> not#(y)
   not#(and(x,y)) -> not#(not(y))
   not#(and(x,y)) -> not#(not(not(y)))
   not#(and(x,y)) -> not#(x)
   not#(and(x,y)) -> not#(not(x))
   not#(and(x,y)) -> not#(not(not(x)))
  TRS:
   not(not(x)) -> x
   not(or(x,y)) -> and(not(not(not(x))),not(not(not(y))))
   not(and(x,y)) -> or(not(not(not(x))),not(not(not(y))))
  Restore Modifier:
   DPs:
    not#(or(x,y)) -> not#(y)
    not#(or(x,y)) -> not#(not(y))
    not#(or(x,y)) -> not#(not(not(y)))
    not#(or(x,y)) -> not#(x)
    not#(or(x,y)) -> not#(not(x))
    not#(or(x,y)) -> not#(not(not(x)))
    not#(and(x,y)) -> not#(y)
    not#(and(x,y)) -> not#(not(y))
    not#(and(x,y)) -> not#(not(not(y)))
    not#(and(x,y)) -> not#(x)
    not#(and(x,y)) -> not#(not(x))
    not#(and(x,y)) -> not#(not(not(x)))
   TRS:
    not(not(x)) -> x
    not(or(x,y)) -> and(not(not(not(x))),not(not(not(y))))
    not(and(x,y)) -> or(not(not(not(x))),not(not(not(y))))
   SCC Processor:
    #sccs: 1
    #rules: 12
    #arcs: 144/144
    DPs:
     not#(or(x,y)) -> not#(y)
     not#(or(x,y)) -> not#(not(y))
     not#(or(x,y)) -> not#(not(not(y)))
     not#(or(x,y)) -> not#(x)
     not#(or(x,y)) -> not#(not(x))
     not#(or(x,y)) -> not#(not(not(x)))
     not#(and(x,y)) -> not#(y)
     not#(and(x,y)) -> not#(not(y))
     not#(and(x,y)) -> not#(not(not(y)))
     not#(and(x,y)) -> not#(x)
     not#(and(x,y)) -> not#(not(x))
     not#(and(x,y)) -> not#(not(not(x)))
    TRS:
     not(not(x)) -> x
     not(or(x,y)) -> and(not(not(not(x))),not(not(not(y))))
     not(and(x,y)) -> or(not(not(not(x))),not(not(not(y))))
    Open