MAYBE

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

Proof:
 DP Processor:
  DPs:
   and#(x,or(y,z)) -> and#(x,z)
   and#(x,or(y,z)) -> and#(x,y)
   and#(x,or(y,z)) -> or#(and(x,y),and(x,z))
   and#(x,and(y,y)) -> and#(x,y)
   or#(x,or(y,y)) -> or#(x,y)
  TRS:
   and(x,or(y,z)) -> or(and(x,y),and(x,z))
   and(x,and(y,y)) -> and(x,y)
   or(or(x,y),and(y,z)) -> or(x,y)
   or(x,and(x,y)) -> x
   or(true(),y) -> true()
   or(x,false()) -> x
   or(x,x) -> x
   or(x,or(y,y)) -> or(x,y)
   and(x,true()) -> x
   and(false(),y) -> false()
   and(x,x) -> x
  CDG Processor:
   DPs:
    and#(x,or(y,z)) -> and#(x,z)
    and#(x,or(y,z)) -> and#(x,y)
    and#(x,or(y,z)) -> or#(and(x,y),and(x,z))
    and#(x,and(y,y)) -> and#(x,y)
    or#(x,or(y,y)) -> or#(x,y)
   TRS:
    and(x,or(y,z)) -> or(and(x,y),and(x,z))
    and(x,and(y,y)) -> and(x,y)
    or(or(x,y),and(y,z)) -> or(x,y)
    or(x,and(x,y)) -> x
    or(true(),y) -> true()
    or(x,false()) -> x
    or(x,x) -> x
    or(x,or(y,y)) -> or(x,y)
    and(x,true()) -> x
    and(false(),y) -> false()
    and(x,x) -> x
   graph:
    or#(x,or(y,y)) -> or#(x,y) -> or#(x,or(y,y)) -> or#(x,y)
    and#(x,and(y,y)) -> and#(x,y) -> and#(x,or(y,z)) -> and#(x,z)
    and#(x,and(y,y)) -> and#(x,y) -> and#(x,or(y,z)) -> and#(x,y)
    and#(x,and(y,y)) -> and#(x,y) ->
    and#(x,or(y,z)) -> or#(and(x,y),and(x,z))
    and#(x,and(y,y)) -> and#(x,y) ->
    and#(x,and(y,y)) -> and#(x,y)
    and#(x,or(y,z)) -> or#(and(x,y),and(x,z)) ->
    or#(x,or(y,y)) -> or#(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#(x,or(y,z)) -> or#(and(x,y),and(x,z))
    and#(x,or(y,z)) -> and#(x,z) -> and#(x,and(y,y)) -> 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#(x,or(y,z)) -> or#(and(x,y),and(x,z))
    and#(x,or(y,z)) -> and#(x,y) -> and#(x,and(y,y)) -> and#(x,y)
   Restore Modifier:
    DPs:
     and#(x,or(y,z)) -> and#(x,z)
     and#(x,or(y,z)) -> and#(x,y)
     and#(x,or(y,z)) -> or#(and(x,y),and(x,z))
     and#(x,and(y,y)) -> and#(x,y)
     or#(x,or(y,y)) -> or#(x,y)
    TRS:
     and(x,or(y,z)) -> or(and(x,y),and(x,z))
     and(x,and(y,y)) -> and(x,y)
     or(or(x,y),and(y,z)) -> or(x,y)
     or(x,and(x,y)) -> x
     or(true(),y) -> true()
     or(x,false()) -> x
     or(x,x) -> x
     or(x,or(y,y)) -> or(x,y)
     and(x,true()) -> x
     and(false(),y) -> false()
     and(x,x) -> x
    SCC Processor:
     #sccs: 2
     #rules: 4
     #arcs: 14/25
     DPs:
      and#(x,and(y,y)) -> and#(x,y)
      and#(x,or(y,z)) -> and#(x,y)
      and#(x,or(y,z)) -> and#(x,z)
     TRS:
      and(x,or(y,z)) -> or(and(x,y),and(x,z))
      and(x,and(y,y)) -> and(x,y)
      or(or(x,y),and(y,z)) -> or(x,y)
      or(x,and(x,y)) -> x
      or(true(),y) -> true()
      or(x,false()) -> x
      or(x,x) -> x
      or(x,or(y,y)) -> or(x,y)
      and(x,true()) -> x
      and(false(),y) -> false()
      and(x,x) -> x
     Open
     
     DPs:
      or#(x,or(y,y)) -> or#(x,y)
     TRS:
      and(x,or(y,z)) -> or(and(x,y),and(x,z))
      and(x,and(y,y)) -> and(x,y)
      or(or(x,y),and(y,z)) -> or(x,y)
      or(x,and(x,y)) -> x
      or(true(),y) -> true()
      or(x,false()) -> x
      or(x,x) -> x
      or(x,or(y,y)) -> or(x,y)
      and(x,true()) -> x
      and(false(),y) -> false()
      and(x,x) -> x
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [or#](x0, x1) = x1 + 1,
       
       [false] = 0,
       
       [true] = 0,
       
       [and](x0, x1) = x0 + x1,
       
       [or](x0, x1) = x0 + 1
      orientation:
       or#(x,or(y,y)) = y + 2 >= y + 1 = or#(x,y)
       
       and(x,or(y,z)) = x + y + 1 >= x + y + 1 = or(and(x,y),and(x,z))
       
       and(x,and(y,y)) = x + 2y >= x + y = and(x,y)
       
       or(or(x,y),and(y,z)) = x + 2 >= x + 1 = or(x,y)
       
       or(x,and(x,y)) = x + 1 >= x = x
       
       or(true(),y) = 1 >= 0 = true()
       
       or(x,false()) = x + 1 >= x = x
       
       or(x,x) = x + 1 >= x = x
       
       or(x,or(y,y)) = x + 1 >= x + 1 = or(x,y)
       
       and(x,true()) = x >= x = x
       
       and(false(),y) = y >= 0 = false()
       
       and(x,x) = 2x >= x = x
      problem:
       DPs:
        
       TRS:
        and(x,or(y,z)) -> or(and(x,y),and(x,z))
        and(x,and(y,y)) -> and(x,y)
        or(or(x,y),and(y,z)) -> or(x,y)
        or(x,and(x,y)) -> x
        or(true(),y) -> true()
        or(x,false()) -> x
        or(x,x) -> x
        or(x,or(y,y)) -> or(x,y)
        and(x,true()) -> x
        and(false(),y) -> false()
        and(x,x) -> x
      Qed