YES Problem: f(x,y,w,w,a()) -> g1(x,x,y,w) f(x,y,w,a(),a()) -> g1(y,x,x,w) f(x,y,a(),a(),w) -> g2(x,y,y,w) f(x,y,a(),w,w) -> g2(y,y,x,w) g1(x,x,y,a()) -> h(x,y) g1(y,x,x,a()) -> h(x,y) g2(x,y,y,a()) -> h(x,y) g2(y,y,x,a()) -> h(x,y) h(x,x) -> x Proof: DP Processor: DPs: f#(x,y,w,w,a()) -> g1#(x,x,y,w) f#(x,y,w,a(),a()) -> g1#(y,x,x,w) f#(x,y,a(),a(),w) -> g2#(x,y,y,w) f#(x,y,a(),w,w) -> g2#(y,y,x,w) g1#(x,x,y,a()) -> h#(x,y) g1#(y,x,x,a()) -> h#(x,y) g2#(x,y,y,a()) -> h#(x,y) g2#(y,y,x,a()) -> h#(x,y) TRS: f(x,y,w,w,a()) -> g1(x,x,y,w) f(x,y,w,a(),a()) -> g1(y,x,x,w) f(x,y,a(),a(),w) -> g2(x,y,y,w) f(x,y,a(),w,w) -> g2(y,y,x,w) g1(x,x,y,a()) -> h(x,y) g1(y,x,x,a()) -> h(x,y) g2(x,y,y,a()) -> h(x,y) g2(y,y,x,a()) -> h(x,y) h(x,x) -> x TDG Processor: DPs: f#(x,y,w,w,a()) -> g1#(x,x,y,w) f#(x,y,w,a(),a()) -> g1#(y,x,x,w) f#(x,y,a(),a(),w) -> g2#(x,y,y,w) f#(x,y,a(),w,w) -> g2#(y,y,x,w) g1#(x,x,y,a()) -> h#(x,y) g1#(y,x,x,a()) -> h#(x,y) g2#(x,y,y,a()) -> h#(x,y) g2#(y,y,x,a()) -> h#(x,y) TRS: f(x,y,w,w,a()) -> g1(x,x,y,w) f(x,y,w,a(),a()) -> g1(y,x,x,w) f(x,y,a(),a(),w) -> g2(x,y,y,w) f(x,y,a(),w,w) -> g2(y,y,x,w) g1(x,x,y,a()) -> h(x,y) g1(y,x,x,a()) -> h(x,y) g2(x,y,y,a()) -> h(x,y) g2(y,y,x,a()) -> h(x,y) h(x,x) -> x graph: f#(x,y,a(),a(),w) -> g2#(x,y,y,w) -> g2#(y,y,x,a()) -> h#(x,y) f#(x,y,a(),a(),w) -> g2#(x,y,y,w) -> g2#(x,y,y,a()) -> h#(x,y) f#(x,y,a(),w,w) -> g2#(y,y,x,w) -> g2#(y,y,x,a()) -> h#(x,y) f#(x,y,a(),w,w) -> g2#(y,y,x,w) -> g2#(x,y,y,a()) -> h#(x,y) f#(x,y,w,a(),a()) -> g1#(y,x,x,w) -> g1#(y,x,x,a()) -> h#(x,y) f#(x,y,w,a(),a()) -> g1#(y,x,x,w) -> g1#(x,x,y,a()) -> h#(x,y) f#(x,y,w,w,a()) -> g1#(x,x,y,w) -> g1#(y,x,x,a()) -> h#(x,y) f#(x,y,w,w,a()) -> g1#(x,x,y,w) -> g1#(x,x,y,a()) -> h#(x,y) SCC Processor: #sccs: 0 #rules: 0 #arcs: 8/64