YES Time: 0.738 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: g(fAC(x,y)) -> fAC(g(x),g(y)) fAC(a(),g(g(a()))) -> fAC(g(a()),g(a())) 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: g#(fAC(x,y)) -> g#(y) g#(fAC(x,y)) -> g#(x) g#(fAC(x,y)) -> f{AC,#}(g(x),g(y)) f{AC,#}(a(),g(g(a()))) -> f{AC,#}(g(a()),g(a())) f{AC,#}(x6,fAC(a(),g(g(a())))) -> f{AC,#}(g(a()),g(a())) f{AC,#}(x6,fAC(a(),g(g(a())))) -> f{AC,#}(x6,fAC(g(a()),g(a()))) 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: g(fAC(x,y)) -> fAC(g(x),g(y)) fAC(a(),g(g(a()))) -> fAC(g(a()),g(a())) S: f{AC,#}(fAC(x7,x8),x9) -> f{AC,#}(x7,x8) f{AC,#}(x7,fAC(x8,x9)) -> f{AC,#}(x8,x9) 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: g#(fAC(x,y)) -> g#(y) g#(fAC(x,y)) -> g#(x) g#(fAC(x,y)) -> f{AC,#}(g(x),g(y)) f{AC,#}(a(),g(g(a()))) -> f{AC,#}(g(a()),g(a())) f{AC,#}(x6,fAC(a(),g(g(a())))) -> f{AC,#}(g(a()),g(a())) f{AC,#}(x6,fAC(a(),g(g(a())))) -> f{AC,#}(x6,fAC(g(a()),g(a()))) 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: g(fAC(x,y)) -> fAC(g(x),g(y)) fAC(a(),g(g(a()))) -> fAC(g(a()),g(a())) S: f{AC,#}(fAC(x7,x8),x9) -> f{AC,#}(x7,x8) f{AC,#}(x7,fAC(x8,x9)) -> f{AC,#}(x8,x9) SCC Processor: #sccs: 2 #rules: 5 #arcs: 18/36 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: g#(fAC(x,y)) -> g#(y) g#(fAC(x,y)) -> g#(x) 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: g(fAC(x,y)) -> fAC(g(x),g(y)) fAC(a(),g(g(a()))) -> fAC(g(a()),g(a())) S: f{AC,#}(fAC(x7,x8),x9) -> f{AC,#}(x7,x8) f{AC,#}(x7,fAC(x8,x9)) -> f{AC,#}(x8,x9) AC-DP unlabeling: 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) DPs: g#(fAC(x,y)) -> g#(y) g#(fAC(x,y)) -> g#(x) 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: g(fAC(x,y)) -> fAC(g(x),g(y)) fAC(a(),g(g(a()))) -> fAC(g(a()),g(a())) S: fAC(fAC(x7,x8),x9) -> fAC(x7,x8) fAC(x7,fAC(x8,x9)) -> fAC(x8,x9) Usable Rule Processor: 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) DPs: g#(fAC(x,y)) -> g#(y) g#(fAC(x,y)) -> g#(x) 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: S: fAC(fAC(x7,x8),x9) -> fAC(x7,x8) fAC(x7,fAC(x8,x9)) -> fAC(x8,x9) AC-RPO Processor: argument filtering: pi(fAC) = [0,1] pi(g#) = [0] precedence: fAC > g# status: 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) DPs: 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: S: fAC(fAC(x7,x8),x9) -> fAC(x7,x8) fAC(x7,fAC(x8,x9)) -> fAC(x8,x9) Qed 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,#}(a(),g(g(a()))) -> f{AC,#}(g(a()),g(a())) f{AC,#}(x6,fAC(a(),g(g(a())))) -> f{AC,#}(x6,fAC(g(a()),g(a()))) f{AC,#}(x6,fAC(a(),g(g(a())))) -> f{AC,#}(g(a()),g(a())) 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: g(fAC(x,y)) -> fAC(g(x),g(y)) fAC(a(),g(g(a()))) -> fAC(g(a()),g(a())) S: f{AC,#}(fAC(x7,x8),x9) -> f{AC,#}(x7,x8) f{AC,#}(x7,fAC(x8,x9)) -> f{AC,#}(x8,x9) AC-DP unlabeling: 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) DPs: fAC(a(),g(g(a()))) -> fAC(g(a()),g(a())) fAC(x6,fAC(a(),g(g(a())))) -> fAC(x6,fAC(g(a()),g(a()))) fAC(x6,fAC(a(),g(g(a())))) -> fAC(g(a()),g(a())) 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: g(fAC(x,y)) -> fAC(g(x),g(y)) fAC(a(),g(g(a()))) -> fAC(g(a()),g(a())) S: fAC(fAC(x7,x8),x9) -> fAC(x7,x8) fAC(x7,fAC(x8,x9)) -> fAC(x8,x9) Usable Rule Processor: 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) DPs: fAC(a(),g(g(a()))) -> fAC(g(a()),g(a())) fAC(x6,fAC(a(),g(g(a())))) -> fAC(x6,fAC(g(a()),g(a()))) fAC(x6,fAC(a(),g(g(a())))) -> fAC(g(a()),g(a())) 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: S: fAC(fAC(x7,x8),x9) -> fAC(x7,x8) fAC(x7,fAC(x8,x9)) -> fAC(x8,x9) AC-RPO Processor: argument filtering: pi(fAC) = [0,1] pi(g) = [] pi(a) = [] precedence: a > g > fAC status: 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) DPs: 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: S: fAC(fAC(x7,x8),x9) -> fAC(x7,x8) fAC(x7,fAC(x8,x9)) -> fAC(x8,x9) Qed