YES Problem: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() Proof: DP Processor: DPs: g#(x,x,x) -> g#(c(),d(),e()) g#(x,y,x) -> g#(c(),d(),e()) s#(f(x,y)) -> s#(x) s#(f(x,y)) -> s#(s(x)) s#(f(x,y)) -> f#(s(s(x)),a()) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) h#(h(x,a()),y) -> h#(a(),x) h#(h(x,a()),y) -> h#(a(),y) h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) f#(x,f(y,f(x,y))) -> f#(y,b()) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) f#(h(a(),y),g(x,b(),a())) -> s#(b()) f#(h(a(),y),g(x,b(),a())) -> s#(y) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) h#(f(x,s(y)),b()) -> s#(x) h#(f(x,s(y)),b()) -> f#(s(x),a()) h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a())) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() TDG Processor: DPs: g#(x,x,x) -> g#(c(),d(),e()) g#(x,y,x) -> g#(c(),d(),e()) s#(f(x,y)) -> s#(x) s#(f(x,y)) -> s#(s(x)) s#(f(x,y)) -> f#(s(s(x)),a()) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) h#(h(x,a()),y) -> h#(a(),x) h#(h(x,a()),y) -> h#(a(),y) h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) f#(x,f(y,f(x,y))) -> f#(y,b()) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) f#(h(a(),y),g(x,b(),a())) -> s#(b()) f#(h(a(),y),g(x,b(),a())) -> s#(y) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) h#(f(x,s(y)),b()) -> s#(x) h#(f(x,s(y)),b()) -> f#(s(x),a()) h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a())) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() graph: h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) -> h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) -> h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a())) h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) -> h#(f(x,s(y)),b()) -> f#(s(x),a()) h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) -> h#(f(x,s(y)),b()) -> s#(x) h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) -> h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) -> h#(h(x,a()),y) -> h#(a(),y) h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) -> h#(h(x,a()),y) -> h#(a(),x) h#(h(x,a()),y) -> h#(a(),y) -> h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) h#(h(x,a()),y) -> h#(a(),y) -> h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a())) h#(h(x,a()),y) -> h#(a(),y) -> h#(f(x,s(y)),b()) -> f#(s(x),a()) h#(h(x,a()),y) -> h#(a(),y) -> h#(f(x,s(y)),b()) -> s#(x) h#(h(x,a()),y) -> h#(a(),y) -> h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) h#(h(x,a()),y) -> h#(a(),y) -> h#(h(x,a()),y) -> h#(a(),y) h#(h(x,a()),y) -> h#(a(),y) -> h#(h(x,a()),y) -> h#(a(),x) h#(h(x,a()),y) -> h#(a(),x) -> h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) h#(h(x,a()),y) -> h#(a(),x) -> h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a())) h#(h(x,a()),y) -> h#(a(),x) -> h#(f(x,s(y)),b()) -> f#(s(x),a()) h#(h(x,a()),y) -> h#(a(),x) -> h#(f(x,s(y)),b()) -> s#(x) h#(h(x,a()),y) -> h#(a(),x) -> h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) h#(h(x,a()),y) -> h#(a(),x) -> h#(h(x,a()),y) -> h#(a(),y) h#(h(x,a()),y) -> h#(a(),x) -> h#(h(x,a()),y) -> h#(a(),x) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) -> f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) -> f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) -> f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) -> f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) -> f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) -> f#(h(a(),y),g(x,b(),a())) -> s#(y) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) -> f#(h(a(),y),g(x,b(),a())) -> s#(b()) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) -> f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) -> f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) -> f#(x,f(y,f(x,y))) -> f#(y,b()) h#(f(x,s(y)),b()) -> f#(s(x),a()) -> f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) h#(f(x,s(y)),b()) -> f#(s(x),a()) -> f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) h#(f(x,s(y)),b()) -> f#(s(x),a()) -> f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) h#(f(x,s(y)),b()) -> f#(s(x),a()) -> f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) h#(f(x,s(y)),b()) -> f#(s(x),a()) -> f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) h#(f(x,s(y)),b()) -> f#(s(x),a()) -> f#(h(a(),y),g(x,b(),a())) -> s#(y) h#(f(x,s(y)),b()) -> f#(s(x),a()) -> f#(h(a(),y),g(x,b(),a())) -> s#(b()) h#(f(x,s(y)),b()) -> f#(s(x),a()) -> f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) h#(f(x,s(y)),b()) -> f#(s(x),a()) -> f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) h#(f(x,s(y)),b()) -> f#(s(x),a()) -> f#(x,f(y,f(x,y))) -> f#(y,b()) h#(f(x,s(y)),b()) -> s#(x) -> s#(f(x,y)) -> f#(y,f(s(s(x)),a())) h#(f(x,s(y)),b()) -> s#(x) -> s#(f(x,y)) -> f#(s(s(x)),a()) h#(f(x,s(y)),b()) -> s#(x) -> s#(f(x,y)) -> s#(s(x)) h#(f(x,s(y)),b()) -> s#(x) -> s#(f(x,y)) -> s#(x) h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a())) -> g#(x,y,x) -> g#(c(),d(),e()) h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a())) -> g#(x,x,x) -> g#(c(),d(),e()) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) -> h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) -> h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a())) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) -> h#(f(x,s(y)),b()) -> f#(s(x),a()) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) -> h#(f(x,s(y)),b()) -> s#(x) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) -> h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) -> h#(h(x,a()),y) -> h#(a(),y) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) -> h#(h(x,a()),y) -> h#(a(),x) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(h(a(),y),g(x,b(),a())) -> s#(y) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(h(a(),y),g(x,b(),a())) -> s#(b()) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(x,f(y,f(x,y))) -> f#(y,b()) f#(h(a(),y),g(x,b(),a())) -> s#(b()) -> s#(f(x,y)) -> f#(y,f(s(s(x)),a())) f#(h(a(),y),g(x,b(),a())) -> s#(b()) -> s#(f(x,y)) -> f#(s(s(x)),a()) f#(h(a(),y),g(x,b(),a())) -> s#(b()) -> s#(f(x,y)) -> s#(s(x)) f#(h(a(),y),g(x,b(),a())) -> s#(b()) -> s#(f(x,y)) -> s#(x) f#(h(a(),y),g(x,b(),a())) -> s#(y) -> s#(f(x,y)) -> f#(y,f(s(s(x)),a())) f#(h(a(),y),g(x,b(),a())) -> s#(y) -> s#(f(x,y)) -> f#(s(s(x)),a()) f#(h(a(),y),g(x,b(),a())) -> s#(y) -> s#(f(x,y)) -> s#(s(x)) f#(h(a(),y),g(x,b(),a())) -> s#(y) -> s#(f(x,y)) -> s#(x) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(h(a(),y),g(x,b(),a())) -> s#(y) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(h(a(),y),g(x,b(),a())) -> s#(b()) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(x,f(y,f(x,y))) -> f#(y,b()) f#(x,f(y,f(x,y))) -> f#(y,b()) -> f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) f#(x,f(y,f(x,y))) -> f#(y,b()) -> f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) f#(x,f(y,f(x,y))) -> f#(y,b()) -> f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) f#(x,f(y,f(x,y))) -> f#(y,b()) -> f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) f#(x,f(y,f(x,y))) -> f#(y,b()) -> f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) f#(x,f(y,f(x,y))) -> f#(y,b()) -> f#(h(a(),y),g(x,b(),a())) -> s#(y) f#(x,f(y,f(x,y))) -> f#(y,b()) -> f#(h(a(),y),g(x,b(),a())) -> s#(b()) f#(x,f(y,f(x,y))) -> f#(y,b()) -> f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) f#(x,f(y,f(x,y))) -> f#(y,b()) -> f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) f#(x,f(y,f(x,y))) -> f#(y,b()) -> f#(x,f(y,f(x,y))) -> f#(y,b()) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) -> f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) -> f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) -> f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) -> f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) -> f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) -> f#(h(a(),y),g(x,b(),a())) -> s#(y) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) -> f#(h(a(),y),g(x,b(),a())) -> s#(b()) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) -> f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) -> f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) -> f#(x,f(y,f(x,y))) -> f#(y,b()) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(f(x,s(y)),b()) -> g#(y,a(),f(s(x),a())) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(f(x,s(y)),b()) -> f#(s(x),a()) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(f(x,s(y)),b()) -> s#(x) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(h(x,a()),y) -> h#(a(),y) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(h(x,a()),y) -> h#(a(),x) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(h(a(),y),g(x,b(),a())) -> s#(y) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(h(a(),y),g(x,b(),a())) -> s#(b()) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(x,f(y,f(x,y))) -> f#(y,b()) f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) -> g#(x,y,x) -> g#(c(),d(),e()) f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) -> g#(x,x,x) -> g#(c(),d(),e()) s#(f(x,y)) -> f#(s(s(x)),a()) -> f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) s#(f(x,y)) -> f#(s(s(x)),a()) -> f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) s#(f(x,y)) -> f#(s(s(x)),a()) -> f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) s#(f(x,y)) -> f#(s(s(x)),a()) -> f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) s#(f(x,y)) -> f#(s(s(x)),a()) -> f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) s#(f(x,y)) -> f#(s(s(x)),a()) -> f#(h(a(),y),g(x,b(),a())) -> s#(y) s#(f(x,y)) -> f#(s(s(x)),a()) -> f#(h(a(),y),g(x,b(),a())) -> s#(b()) s#(f(x,y)) -> f#(s(s(x)),a()) -> f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) s#(f(x,y)) -> f#(s(s(x)),a()) -> f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) s#(f(x,y)) -> f#(s(s(x)),a()) -> f#(x,f(y,f(x,y))) -> f#(y,b()) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) -> f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) -> f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) -> f#(x,g(x,a(),f(s(x),y))) -> g#(a(),b(),y) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) -> f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) -> f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) -> f#(h(a(),y),g(x,b(),a())) -> s#(y) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) -> f#(h(a(),y),g(x,b(),a())) -> s#(b()) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) -> f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) -> f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) -> f#(x,f(y,f(x,y))) -> f#(y,b()) s#(f(x,y)) -> s#(s(x)) -> s#(f(x,y)) -> f#(y,f(s(s(x)),a())) s#(f(x,y)) -> s#(s(x)) -> s#(f(x,y)) -> f#(s(s(x)),a()) s#(f(x,y)) -> s#(s(x)) -> s#(f(x,y)) -> s#(s(x)) s#(f(x,y)) -> s#(s(x)) -> s#(f(x,y)) -> s#(x) s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> f#(y,f(s(s(x)),a())) s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> f#(s(s(x)),a()) s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> s#(s(x)) s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> s#(x) g#(x,y,x) -> g#(c(),d(),e()) -> g#(x,y,x) -> g#(c(),d(),e()) g#(x,y,x) -> g#(c(),d(),e()) -> g#(x,x,x) -> g#(c(),d(),e()) g#(x,x,x) -> g#(c(),d(),e()) -> g#(x,y,x) -> g#(c(),d(),e()) g#(x,x,x) -> g#(c(),d(),e()) -> g#(x,x,x) -> g#(c(),d(),e()) SCC Processor: #sccs: 2 #rules: 21 #arcs: 153/529 DPs: h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) h#(h(x,a()),y) -> h#(a(),x) h#(h(x,a()),y) -> h#(a(),y) h#(f(x,s(y)),b()) -> s#(x) s#(f(x,y)) -> s#(x) s#(f(x,y)) -> s#(s(x)) s#(f(x,y)) -> f#(s(s(x)),a()) f#(x,f(y,f(x,y))) -> f#(y,b()) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) f#(h(a(),y),g(x,b(),a())) -> s#(b()) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) f#(h(a(),y),g(x,b(),a())) -> s#(y) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) h#(f(x,s(y)),b()) -> f#(s(x),a()) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() EDG Processor: DPs: h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) h#(h(x,a()),y) -> h#(a(),x) h#(h(x,a()),y) -> h#(a(),y) h#(f(x,s(y)),b()) -> s#(x) s#(f(x,y)) -> s#(x) s#(f(x,y)) -> s#(s(x)) s#(f(x,y)) -> f#(s(s(x)),a()) f#(x,f(y,f(x,y))) -> f#(y,b()) f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) f#(h(a(),y),g(x,b(),a())) -> s#(b()) s#(f(x,y)) -> f#(y,f(s(s(x)),a())) f#(h(a(),y),g(x,b(),a())) -> s#(y) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) h#(f(x,s(y)),b()) -> f#(s(x),a()) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() graph: h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) -> h#(h(x,a()),y) -> h#(a(),x) h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) -> h#(h(x,a()),y) -> h#(a(),y) h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) -> h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) -> f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) -> f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) h#(f(x,s(y)),b()) -> s#(x) -> s#(f(x,y)) -> s#(x) h#(f(x,s(y)),b()) -> s#(x) -> s#(f(x,y)) -> s#(s(x)) h#(f(x,s(y)),b()) -> s#(x) -> s#(f(x,y)) -> f#(s(s(x)),a()) h#(f(x,s(y)),b()) -> s#(x) -> s#(f(x,y)) -> f#(y,f(s(s(x)),a())) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) -> h#(f(x,s(y)),b()) -> s#(x) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) -> h#(f(x,s(y)),b()) -> f#(s(x),a()) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) -> h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(x,f(y,f(x,y))) -> f#(y,b()) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) -> f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) f#(h(a(),y),g(x,b(),a())) -> s#(y) -> s#(f(x,y)) -> s#(x) f#(h(a(),y),g(x,b(),a())) -> s#(y) -> s#(f(x,y)) -> s#(s(x)) f#(h(a(),y),g(x,b(),a())) -> s#(y) -> s#(f(x,y)) -> f#(s(s(x)),a()) f#(h(a(),y),g(x,b(),a())) -> s#(y) -> s#(f(x,y)) -> f#(y,f(s(s(x)),a())) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(x,f(y,f(x,y))) -> f#(y,b()) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(x,f(y,f(x,y))) -> f#(x,f(y,b())) f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) -> f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(h(x,a()),y) -> h#(a(),x) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(h(x,a()),y) -> h#(a(),y) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(f(x,s(y)),b()) -> s#(x) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(f(x,s(y)),b()) -> f#(s(x),a()) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) -> h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(h(a(),y),g(x,b(),a())) -> s#(b()) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(h(a(),y),g(x,b(),a())) -> s#(y) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(h(a(),y),g(x,b(),a())) -> f#(x,s(y)) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) -> f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) s#(f(x,y)) -> s#(s(x)) -> s#(f(x,y)) -> s#(x) s#(f(x,y)) -> s#(s(x)) -> s#(f(x,y)) -> s#(s(x)) s#(f(x,y)) -> s#(s(x)) -> s#(f(x,y)) -> f#(s(s(x)),a()) s#(f(x,y)) -> s#(s(x)) -> s#(f(x,y)) -> f#(y,f(s(s(x)),a())) s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> s#(x) s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> s#(s(x)) s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> f#(s(s(x)),a()) s#(f(x,y)) -> s#(x) -> s#(f(x,y)) -> f#(y,f(s(s(x)),a())) SCC Processor: #sccs: 4 #rules: 8 #arcs: 40/361 DPs: h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() Usable Rule Processor: DPs: h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) f#(x,g(x,a(),f(s(x),y))) -> h#(x,b()) TRS: s(f(x,y)) -> f(y,f(s(s(x)),a())) s(y) -> b() g(x,y,x) -> g(c(),d(),e()) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) Arctic Interpretation Processor: dimension: 1 usable rules: s(f(x,y)) -> f(y,f(s(s(x)),a())) s(y) -> b() h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) interpretation: [h#](x0, x1) = 1x0 + 1x1 + 0, [f#](x0, x1) = 2x0 + 4, [b] = 2, [h](x0, x1) = x0 + x1 + 0, [a] = 0, [s](x0) = 1x0 + 3, [f](x0, x1) = 3, [e] = 1, [d] = 3, [c] = 0, [g](x0, x1, x2) = 2x0 orientation: h#(f(x,s(y)),b()) = 4 >= 4 = f#(a(),g(y,a(),f(s(x),a()))) f#(x,g(x,a(),f(s(x),y))) = 2x + 4 >= 2x + 4 = f#(h(x,b()),g(a(),b(),y)) f#(h(a(),y),g(x,b(),a())) = 2y + 4 >= 4 = h#(f(x,s(y)),s(b())) f#(x,g(x,a(),f(s(x),y))) = 2x + 4 >= 1x + 3 = h#(x,b()) s(f(x,y)) = 4 >= 3 = f(y,f(s(s(x)),a())) s(y) = 1y + 3 >= 2 = b() g(x,y,x) = 2x >= 2 = g(c(),d(),e()) h(h(x,a()),y) = x + y + 0 >= x + y + 0 = h(h(a(),y),h(a(),x)) h(f(x,s(y)),b()) = 3 >= 3 = f(a(),g(y,a(),f(s(x),a()))) f(x,f(y,f(x,y))) = 3 >= 3 = f(a(),f(x,f(y,b()))) f(x,g(x,a(),f(s(x),y))) = 3 >= 3 = f(h(x,b()),g(a(),b(),y)) f(h(a(),y),g(x,b(),a())) = 3 >= 3 = h(f(x,s(y)),s(b())) problem: DPs: h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) TRS: s(f(x,y)) -> f(y,f(s(s(x)),a())) s(y) -> b() g(x,y,x) -> g(c(),d(),e()) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) Restore Modifier: DPs: h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(x,g(x,a(),f(s(x),y))) -> f#(h(x,b()),g(a(),b(),y)) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {7} transitions: d0() -> 9* e0() -> 8* f130() -> 8* f{#,0}(10,52) -> 7* f{#,0}(12,52) -> 7* f{#,0}(10,31) -> 7* f{#,0}(12,11) -> 7* a0() -> 10* g0(54,10,55) -> 31* g0(9,10,55) -> 31* g0(10,54,10) -> 11* g0(10,9,10) -> 11* g0(8,10,55) -> 41* g0(8,10,40) -> 41* g0(10,54,8) -> 52* g0(10,9,8) -> 52*,41,31,11 g0(54,10,30) -> 31* g0(9,10,30) -> 31* f0(10,52) -> 12* f0(10,54) -> 22* f0(10,56) -> 22* f0(54,10) -> 55*,50,40,30 f0(49,10) -> 50* f0(39,10) -> 40* f0(29,10) -> 30* f0(12,52) -> 12* f0(8,55) -> 39* f0(56,10) -> 50* f0(10,21) -> 22* f0(10,31) -> 12* f0(10,41) -> 12* f0(55,55) -> 49* f0(50,55) -> 49* f0(12,11) -> 12* f0(10,53) -> 22* f0(8,50) -> 39* f0(55,50) -> 49* f0(50,50) -> 49* s0(10) -> 29* s0(54) -> 56*,49 s0(39) -> 49* s0(9) -> 53*,21,20 s0(8) -> 39* h0(10,54) -> 12* h0(22,20) -> 12* h0(8,9) -> 12* h0(12,36) -> 12* h0(22,54) -> 12* h0(22,56) -> 12* h0(10,9) -> 12* h0(54,54) -> 12* h0(9,54) -> 12* h0(54,9) -> 12* h0(9,9) -> 12* h0(22,53) -> 12* h0(10,8) -> 36* h0(8,54) -> 12* b0() -> 56,53,54*,49,39,29,20,21,9 h{#,0}(22,20) -> 7* h{#,0}(22,54) -> 7* h{#,0}(22,56) -> 7* h{#,0}(22,53) -> 7* c0() -> 10* problem: DPs: h#(f(x,s(y)),b()) -> f#(a(),g(y,a(),f(s(x),a()))) f#(h(a(),y),g(x,b(),a())) -> h#(f(x,s(y)),s(b())) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() SCC Processor: #sccs: 0 #rules: 0 #arcs: 5/4 DPs: f#(x,f(y,f(x,y))) -> f#(a(),f(x,f(y,b()))) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {1} transitions: f260() -> 3* f{#,1}(6,5) -> 1* a1() -> 6* f1(6,4) -> 5* f1(2,2) -> 4* f0(6,2) -> 4* f0(3,2) -> 4* f0(3,4) -> 5* f0(2,4) -> 5* b1() -> 2* problem: DPs: TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() Qed DPs: s#(f(x,y)) -> s#(s(x)) s#(f(x,y)) -> s#(x) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() Bounds Processor: bound: 1 enrichment: match-dp automaton: final states: {1} transitions: a0() -> 6* f320() -> 2* s{#,0}(2) -> 1* s{#,0}(14) -> 1* s{#,0}(11) -> 1* s{#,0}(13) -> 1* s{#,0}(3) -> 1* f0(14,6) -> 8* f0(11,6) -> 8* f0(8,8) -> 7* f0(7,6) -> 8* f0(2,8) -> 3* s{#,1}(12) -> 1* s{#,1}(14) -> 1* s{#,1}(13) -> 1* s0(14) -> 7* s0(11) -> 7* s0(13) -> 7* s0(3) -> 7* s1(2) -> 13*,3,12 b1() -> 13,11,14*,3,7 problem: DPs: s#(f(x,y)) -> s#(x) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: s{#,0}(2) -> 1* f370() -> 2* problem: DPs: TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() Qed DPs: h#(h(x,a()),y) -> h#(h(a(),y),h(a(),x)) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {1} transitions: a0() -> 3* f390() -> 2* h0(3,3) -> 6* h0(3,9) -> 7* h0(3,2) -> 9*,5,4 h0(3,4) -> 7* h{#,0}(9,4) -> 1* h{#,0}(5,9) -> 1* h{#,0}(9,9) -> 1* h{#,0}(5,4) -> 1* h{#,0}(7,6) -> 1* problem: DPs: TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() Qed DPs: g#(x,x,x) -> g#(c(),d(),e()) g#(x,y,x) -> g#(c(),d(),e()) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() EDG Processor: DPs: g#(x,x,x) -> g#(c(),d(),e()) g#(x,y,x) -> g#(c(),d(),e()) TRS: g(x,x,x) -> g(c(),d(),e()) g(x,y,x) -> g(c(),d(),e()) s(f(x,y)) -> f(y,f(s(s(x)),a())) h(h(x,a()),y) -> h(h(a(),y),h(a(),x)) f(x,f(y,f(x,y))) -> f(a(),f(x,f(y,b()))) f(h(a(),y),g(x,b(),a())) -> h(f(x,s(y)),s(b())) h(f(x,s(y)),b()) -> f(a(),g(y,a(),f(s(x),a()))) f(x,g(x,a(),f(s(x),y))) -> f(h(x,b()),g(a(),b(),y)) s(y) -> b() graph: SCC Processor: #sccs: 0 #rules: 0 #arcs: 0/4