YES

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

Proof:
 DP Processor:
  DPs:
   not#(or(x,y)) -> not#(y)
   not#(or(x,y)) -> not#(x)
   not#(or(x,y)) -> and#(not(x),not(y))
   not#(and(x,y)) -> not#(y)
   not#(and(x,y)) -> not#(x)
   and#(x,or(y,z)) -> and#(x,z)
   and#(x,or(y,z)) -> and#(x,y)
   and#(or(y,z),x) -> and#(x,z)
   and#(or(y,z),x) -> and#(x,y)
  TRS:
   not(not(x)) -> x
   not(or(x,y)) -> and(not(x),not(y))
   not(and(x,y)) -> or(not(x),not(y))
   and(x,or(y,z)) -> or(and(x,y),and(x,z))
   and(or(y,z),x) -> or(and(x,y),and(x,z))
  EDG Processor:
   DPs:
    not#(or(x,y)) -> not#(y)
    not#(or(x,y)) -> not#(x)
    not#(or(x,y)) -> and#(not(x),not(y))
    not#(and(x,y)) -> not#(y)
    not#(and(x,y)) -> not#(x)
    and#(x,or(y,z)) -> and#(x,z)
    and#(x,or(y,z)) -> and#(x,y)
    and#(or(y,z),x) -> and#(x,z)
    and#(or(y,z),x) -> and#(x,y)
   TRS:
    not(not(x)) -> x
    not(or(x,y)) -> and(not(x),not(y))
    not(and(x,y)) -> or(not(x),not(y))
    and(x,or(y,z)) -> or(and(x,y),and(x,z))
    and(or(y,z),x) -> or(and(x,y),and(x,z))
   graph:
    and#(or(y,z),x) -> and#(x,z) -> and#(x,or(y,z)) -> and#(x,z)
    and#(or(y,z),x) -> and#(x,z) -> and#(x,or(y,z)) -> and#(x,y)
    and#(or(y,z),x) -> and#(x,z) -> and#(or(y,z),x) -> and#(x,z)
    and#(or(y,z),x) -> and#(x,z) -> and#(or(y,z),x) -> and#(x,y)
    and#(or(y,z),x) -> and#(x,y) -> and#(x,or(y,z)) -> and#(x,z)
    and#(or(y,z),x) -> and#(x,y) -> and#(x,or(y,z)) -> and#(x,y)
    and#(or(y,z),x) -> and#(x,y) -> and#(or(y,z),x) -> and#(x,z)
    and#(or(y,z),x) -> and#(x,y) -> and#(or(y,z),x) -> and#(x,y)
    and#(x,or(y,z)) -> and#(x,z) -> and#(x,or(y,z)) -> and#(x,z)
    and#(x,or(y,z)) -> and#(x,z) -> and#(x,or(y,z)) -> and#(x,y)
    and#(x,or(y,z)) -> and#(x,z) -> and#(or(y,z),x) -> and#(x,z)
    and#(x,or(y,z)) -> and#(x,z) -> and#(or(y,z),x) -> and#(x,y)
    and#(x,or(y,z)) -> and#(x,y) -> and#(x,or(y,z)) -> and#(x,z)
    and#(x,or(y,z)) -> and#(x,y) -> and#(x,or(y,z)) -> and#(x,y)
    and#(x,or(y,z)) -> and#(x,y) -> and#(or(y,z),x) -> and#(x,z)
    and#(x,or(y,z)) -> and#(x,y) -> and#(or(y,z),x) -> and#(x,y)
    not#(and(x,y)) -> not#(y) -> not#(or(x,y)) -> not#(y)
    not#(and(x,y)) -> not#(y) -> not#(or(x,y)) -> not#(x)
    not#(and(x,y)) -> not#(y) -> not#(or(x,y)) -> and#(not(x),not(y))
    not#(and(x,y)) -> not#(y) -> not#(and(x,y)) -> not#(y)
    not#(and(x,y)) -> not#(y) -> not#(and(x,y)) -> not#(x)
    not#(and(x,y)) -> not#(x) -> not#(or(x,y)) -> not#(y)
    not#(and(x,y)) -> not#(x) -> not#(or(x,y)) -> not#(x)
    not#(and(x,y)) -> not#(x) -> not#(or(x,y)) -> and#(not(x),not(y))
    not#(and(x,y)) -> not#(x) -> not#(and(x,y)) -> not#(y)
    not#(and(x,y)) -> not#(x) -> not#(and(x,y)) -> not#(x)
    not#(or(x,y)) -> and#(not(x),not(y)) ->
    and#(x,or(y,z)) -> and#(x,z)
    not#(or(x,y)) -> and#(not(x),not(y)) ->
    and#(x,or(y,z)) -> and#(x,y)
    not#(or(x,y)) -> and#(not(x),not(y)) ->
    and#(or(y,z),x) -> and#(x,z)
    not#(or(x,y)) -> and#(not(x),not(y)) -> and#(or(y,z),x) -> and#(x,y)
    not#(or(x,y)) -> not#(y) -> not#(or(x,y)) -> not#(y)
    not#(or(x,y)) -> not#(y) -> not#(or(x,y)) -> not#(x)
    not#(or(x,y)) -> not#(y) -> not#(or(x,y)) -> and#(not(x),not(y))
    not#(or(x,y)) -> not#(y) -> not#(and(x,y)) -> not#(y)
    not#(or(x,y)) -> not#(y) -> not#(and(x,y)) -> not#(x)
    not#(or(x,y)) -> not#(x) -> not#(or(x,y)) -> not#(y)
    not#(or(x,y)) -> not#(x) -> not#(or(x,y)) -> not#(x)
    not#(or(x,y)) -> not#(x) -> not#(or(x,y)) -> and#(not(x),not(y))
    not#(or(x,y)) -> not#(x) -> not#(and(x,y)) -> not#(y)
    not#(or(x,y)) -> not#(x) -> not#(and(x,y)) -> not#(x)
   SCC Processor:
    #sccs: 2
    #rules: 8
    #arcs: 40/81
    DPs:
     not#(and(x,y)) -> not#(y)
     not#(and(x,y)) -> not#(x)
     not#(or(x,y)) -> not#(x)
     not#(or(x,y)) -> not#(y)
    TRS:
     not(not(x)) -> x
     not(or(x,y)) -> and(not(x),not(y))
     not(and(x,y)) -> or(not(x),not(y))
     and(x,or(y,z)) -> or(and(x,y),and(x,z))
     and(or(y,z),x) -> or(and(x,y),and(x,z))
    Subterm Criterion Processor:
     simple projection:
      pi(not#) = 0
     problem:
      DPs:
       
      TRS:
       not(not(x)) -> x
       not(or(x,y)) -> and(not(x),not(y))
       not(and(x,y)) -> or(not(x),not(y))
       and(x,or(y,z)) -> or(and(x,y),and(x,z))
       and(or(y,z),x) -> or(and(x,y),and(x,z))
     Qed
    
    DPs:
     and#(or(y,z),x) -> and#(x,z)
     and#(or(y,z),x) -> and#(x,y)
     and#(x,or(y,z)) -> and#(x,y)
     and#(x,or(y,z)) -> and#(x,z)
    TRS:
     not(not(x)) -> x
     not(or(x,y)) -> and(not(x),not(y))
     not(and(x,y)) -> or(not(x),not(y))
     and(x,or(y,z)) -> or(and(x,y),and(x,z))
     and(or(y,z),x) -> or(and(x,y),and(x,z))
    Usable Rule Processor:
     DPs:
      and#(or(y,z),x) -> and#(x,z)
      and#(or(y,z),x) -> and#(x,y)
      and#(x,or(y,z)) -> and#(x,y)
      and#(x,or(y,z)) -> and#(x,z)
     TRS:
      
     Bounds Processor:
      bound: 0
      enrichment: match-dp
      automaton:
       final states: {7}
       transitions:
        f50() -> 8*
        and{#,0}(8,8) -> 7*
      problem:
       DPs:
        and#(or(y,z),x) -> and#(x,z)
        and#(or(y,z),x) -> and#(x,y)
        and#(x,or(y,z)) -> and#(x,y)
       TRS:
        
      Restore Modifier:
       DPs:
        and#(or(y,z),x) -> and#(x,z)
        and#(or(y,z),x) -> and#(x,y)
        and#(x,or(y,z)) -> and#(x,y)
       TRS:
        not(not(x)) -> x
        not(or(x,y)) -> and(not(x),not(y))
        not(and(x,y)) -> or(not(x),not(y))
        and(x,or(y,z)) -> or(and(x,y),and(x,z))
        and(or(y,z),x) -> or(and(x,y),and(x,z))
       Usable Rule Processor:
        DPs:
         and#(or(y,z),x) -> and#(x,z)
         and#(or(y,z),x) -> and#(x,y)
         and#(x,or(y,z)) -> and#(x,y)
        TRS:
         
        Bounds Processor:
         bound: 0
         enrichment: match-dp
         automaton:
          final states: {5}
          transitions:
           f80() -> 6*
           and{#,0}(6,6) -> 5*
         problem:
          DPs:
           and#(or(y,z),x) -> and#(x,z)
           and#(or(y,z),x) -> and#(x,y)
          TRS:
           
         Restore Modifier:
          DPs:
           and#(or(y,z),x) -> and#(x,z)
           and#(or(y,z),x) -> and#(x,y)
          TRS:
           not(not(x)) -> x
           not(or(x,y)) -> and(not(x),not(y))
           not(and(x,y)) -> or(not(x),not(y))
           and(x,or(y,z)) -> or(and(x,y),and(x,z))
           and(or(y,z),x) -> or(and(x,y),and(x,z))
          Usable Rule Processor:
           DPs:
            and#(or(y,z),x) -> and#(x,z)
            and#(or(y,z),x) -> and#(x,y)
           TRS:
            
           Bounds Processor:
            bound: 0
            enrichment: match-dp
            automaton:
             final states: {3}
             transitions:
              f100() -> 4*
              and{#,0}(4,4) -> 3*
            problem:
             DPs:
              and#(or(y,z),x) -> and#(x,z)
             TRS:
              
            Restore Modifier:
             DPs:
              and#(or(y,z),x) -> and#(x,z)
             TRS:
              not(not(x)) -> x
              not(or(x,y)) -> and(not(x),not(y))
              not(and(x,y)) -> or(not(x),not(y))
              and(x,or(y,z)) -> or(and(x,y),and(x,z))
              and(or(y,z),x) -> or(and(x,y),and(x,z))
             Usable Rule Processor:
              DPs:
               and#(or(y,z),x) -> and#(x,z)
              TRS:
               
              Bounds Processor:
               bound: 0
               enrichment: match-dp
               automaton:
                final states: {1}
                transitions:
                 and{#,0}(2,2) -> 1*
                 f120() -> 2*
               problem:
                DPs:
                 
                TRS:
                 
               Qed