YES 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 TDG 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,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)) 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)) -> and#(x,z) 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,and(y,y)) -> 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,or(y,z)) -> 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,y) -> and#(x,and(y,y)) -> 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,or(y,z)) -> and#(x,y) and#(x,or(y,z)) -> and#(x,y) -> and#(x,or(y,z)) -> and#(x,z) 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,z) and#(x,or(y,z)) -> and#(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 LPO Processor: argument filtering: pi(or) = [0,1] pi(and) = [0,1] pi(true) = [] pi(false) = [] pi(and#) = 1 precedence: and > and# ~ false ~ true ~ or 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 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 KBO Processor: argument filtering: pi(or) = [0] pi(and) = [0,1] pi(true) = [] pi(false) = [] pi(or#) = 1 weight function: w0 = 1 w(or#) = w(false) = w(true) = w(and) = w(or) = 1 precedence: or# ~ false ~ true > and > or 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