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: 1
      enrichment: match-dp
      automaton:
       final states: {16}
       transitions:
        and{#,0}(13,13) -> 14*
        and{#,0}(14,14) -> 14*
        and{#,0}(15,15) -> 16*
        and{#,0}(13,14) -> 14*
        and{#,0}(14,13) -> 14*
        or0(13,13) -> 13*
        or0(14,14) -> 13*
        or0(13,14) -> 13*
        or0(14,13) -> 13*
        and{#,1}(13,13) -> 14*
        and{#,1}(14,14) -> 14*
        and{#,1}(15,13) -> 16*
        and{#,1}(13,14) -> 14*
        and{#,1}(14,13) -> 14*
        and{#,1}(15,14) -> 16*
        13 -> 15*
        14 -> 15*
      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: 1
         enrichment: match-dp
         automaton:
          final states: {8}
          transitions:
           and{#,0}(5,5) -> 6*
           and{#,0}(6,6) -> 6*
           and{#,0}(7,7) -> 8*
           and{#,0}(5,6) -> 6*
           and{#,0}(6,5) -> 6*
           or0(5,5) -> 5*
           or0(6,6) -> 5*
           or0(5,6) -> 5*
           or0(6,5) -> 5*
           and{#,1}(5,5) -> 6*
           and{#,1}(6,6) -> 6*
           and{#,1}(7,5) -> 8*
           and{#,1}(5,6) -> 6*
           and{#,1}(6,5) -> 6*
           and{#,1}(7,6) -> 8*
           5 -> 7*
           6 -> 7*
         problem:
          DPs:
           and#(or(y,z),x) -> and#(x,z)
           and#(x,or(y,z)) -> and#(x,y)
          TRS:
           
         Restore Modifier:
          DPs:
           and#(or(y,z),x) -> and#(x,z)
           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#(x,or(y,z)) -> and#(x,y)
           TRS:
            
           Bounds Processor:
            bound: 1
            enrichment: match-dp
            automaton:
             final states: {8}
             transitions:
              and{#,0}(5,5) -> 6*
              and{#,0}(6,6) -> 6*
              and{#,0}(7,7) -> 8*
              and{#,0}(5,6) -> 6*
              and{#,0}(6,5) -> 6*
              or0(5,5) -> 5*
              or0(6,6) -> 5*
              or0(5,6) -> 5*
              or0(6,5) -> 5*
              and{#,1}(5,5) -> 6*
              and{#,1}(6,6) -> 6*
              and{#,1}(7,5) -> 8*
              and{#,1}(5,6) -> 6*
              and{#,1}(6,5) -> 6*
              and{#,1}(7,6) -> 8*
              5 -> 7*
              6 -> 7*
            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: 1
               enrichment: match-dp
               automaton:
                final states: {2}
                transitions:
                 and{#,0}(1,1) -> 2*
                 or0(1,1) -> 1*
                 and{#,1}(1,1) -> 2*
               problem:
                DPs:
                 
                TRS:
                 
               Qed