MAYBE Time: 0.381 Problem: Equations: fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5)) fAC(x3,x4) -> fAC(x4,x3) fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5) fAC(x4,x3) -> fAC(x3,x4) TRS: fAC(x,g(y,z)) -> g(fAC(x,y),fAC(x,z)) fAC(x,u1(y)) -> u1(fAC(x,y)) fAC(x,u2(y)) -> u2(fAC(x,y)) u1(g(x,y)) -> g(u1(x),u1(y)) u2(g(x,y)) -> g(u2(x),u2(y)) u2(u1(x)) -> u1(u2(x)) Proof: DP Processor: Equations#: f{AC,#}(fAC(x3,x4),x5) -> f{AC,#}(x3,fAC(x4,x5)) f{AC,#}(x3,x4) -> f{AC,#}(x4,x3) f{AC,#}(x3,fAC(x4,x5)) -> f{AC,#}(fAC(x3,x4),x5) f{AC,#}(x4,x3) -> f{AC,#}(x3,x4) DPs: f{AC,#}(x,g(y,z)) -> f{AC,#}(x,z) f{AC,#}(x,g(y,z)) -> f{AC,#}(x,y) f{AC,#}(x,u1(y)) -> f{AC,#}(x,y) f{AC,#}(x,u1(y)) -> u1#(fAC(x,y)) f{AC,#}(x,u2(y)) -> f{AC,#}(x,y) f{AC,#}(x,u2(y)) -> u2#(fAC(x,y)) u1#(g(x,y)) -> u1#(y) u1#(g(x,y)) -> u1#(x) u2#(g(x,y)) -> u2#(y) u2#(g(x,y)) -> u2#(x) u2#(u1(x)) -> u2#(x) u2#(u1(x)) -> u1#(u2(x)) f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x,z) f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x,y) f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x6,g(fAC(x,y),fAC(x,z))) f{AC,#}(x7,fAC(x,u1(y))) -> f{AC,#}(x,y) f{AC,#}(x7,fAC(x,u1(y))) -> u1#(fAC(x,y)) f{AC,#}(x7,fAC(x,u1(y))) -> f{AC,#}(x7,u1(fAC(x,y))) f{AC,#}(x8,fAC(x,u2(y))) -> f{AC,#}(x,y) f{AC,#}(x8,fAC(x,u2(y))) -> u2#(fAC(x,y)) f{AC,#}(x8,fAC(x,u2(y))) -> f{AC,#}(x8,u2(fAC(x,y))) Equations: fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5)) fAC(x3,x4) -> fAC(x4,x3) fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5) fAC(x4,x3) -> fAC(x3,x4) TRS: fAC(x,g(y,z)) -> g(fAC(x,y),fAC(x,z)) fAC(x,u1(y)) -> u1(fAC(x,y)) fAC(x,u2(y)) -> u2(fAC(x,y)) u1(g(x,y)) -> g(u1(x),u1(y)) u2(g(x,y)) -> g(u2(x),u2(y)) u2(u1(x)) -> u1(u2(x)) S: f{AC,#}(fAC(x9,x10),x11) -> f{AC,#}(x9,x10) f{AC,#}(x9,fAC(x10,x11)) -> f{AC,#}(x10,x11) AC-EDG Processor: Equations#: f{AC,#}(fAC(x3,x4),x5) -> f{AC,#}(x3,fAC(x4,x5)) f{AC,#}(x3,x4) -> f{AC,#}(x4,x3) f{AC,#}(x3,fAC(x4,x5)) -> f{AC,#}(fAC(x3,x4),x5) f{AC,#}(x4,x3) -> f{AC,#}(x3,x4) DPs: f{AC,#}(x,g(y,z)) -> f{AC,#}(x,z) f{AC,#}(x,g(y,z)) -> f{AC,#}(x,y) f{AC,#}(x,u1(y)) -> f{AC,#}(x,y) f{AC,#}(x,u1(y)) -> u1#(fAC(x,y)) f{AC,#}(x,u2(y)) -> f{AC,#}(x,y) f{AC,#}(x,u2(y)) -> u2#(fAC(x,y)) u1#(g(x,y)) -> u1#(y) u1#(g(x,y)) -> u1#(x) u2#(g(x,y)) -> u2#(y) u2#(g(x,y)) -> u2#(x) u2#(u1(x)) -> u2#(x) u2#(u1(x)) -> u1#(u2(x)) f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x,z) f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x,y) f{AC,#}(x6,fAC(x,g(y,z))) -> f{AC,#}(x6,g(fAC(x,y),fAC(x,z))) f{AC,#}(x7,fAC(x,u1(y))) -> f{AC,#}(x,y) f{AC,#}(x7,fAC(x,u1(y))) -> u1#(fAC(x,y)) f{AC,#}(x7,fAC(x,u1(y))) -> f{AC,#}(x7,u1(fAC(x,y))) f{AC,#}(x8,fAC(x,u2(y))) -> f{AC,#}(x,y) f{AC,#}(x8,fAC(x,u2(y))) -> u2#(fAC(x,y)) f{AC,#}(x8,fAC(x,u2(y))) -> f{AC,#}(x8,u2(fAC(x,y))) Equations: fAC(fAC(x3,x4),x5) -> fAC(x3,fAC(x4,x5)) fAC(x3,x4) -> fAC(x4,x3) fAC(x3,fAC(x4,x5)) -> fAC(fAC(x3,x4),x5) fAC(x4,x3) -> fAC(x3,x4) TRS: fAC(x,g(y,z)) -> g(fAC(x,y),fAC(x,z)) fAC(x,u1(y)) -> u1(fAC(x,y)) fAC(x,u2(y)) -> u2(fAC(x,y)) u1(g(x,y)) -> g(u1(x),u1(y)) u2(g(x,y)) -> g(u2(x),u2(y)) u2(u1(x)) -> u1(u2(x)) S: f{AC,#}(fAC(x9,x10),x11) -> f{AC,#}(x9,x10) f{AC,#}(x9,fAC(x10,x11)) -> f{AC,#}(x10,x11) Open