YES
(ignored inputs)COMMENT the following rules are removed from the original TRS f ( g ( x ) , g ( y ) ) -> f ( g ( x ) , h ( y ) ) f ( h ( x ) , g ( y ) ) -> f ( g ( x ) , g ( y ) )
Rewrite Rules:
   [ h(?x) -> g(?x),
     g(?x) -> h(?x),
     f(?x,?y) -> f(?y,?x),
     f(g(?x),h(?y)) -> f(?x,?y),
     f(h(?x),h(?y)) -> f(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ f(g(?x_3),g(?x)) = f(?x_3,?x),
     f(h(?x_1),h(?y_3)) = f(?x_1,?y_3),
     f(g(?x),h(?y_4)) = f(?y_4,?x),
     f(h(?x_4),g(?x)) = f(?x,?x_4) ]
Outer CPs:
   [ f(h(?y_3),g(?x_3)) = f(?x_3,?y_3),
     f(h(?y_4),h(?x_4)) = f(?y_4,?x_4) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ f(?x_4,?x) = f(g(?x_4),g(?x)),
     f(?y_5,?x) = f(g(?x),h(?y_5)),
     f(?x,?x_5) = f(h(?x_5),g(?x)),
     f(?x,?y_4) = f(h(?x),h(?y_4)),
     f(g(?y),h(?x)) = f(?x,?y),
     f(h(?y),h(?x)) = f(?x,?y),
     f(g(?y),g(?x)) = f(?x,?y),
     f(h(?x),g(?y)) = f(?x,?y),
     f(h(?y),g(?x)) = f(?x,?y),
     f(h(?x),h(?y)) = f(?x,?y),
     f(g(?x),g(?y)) = f(?x,?y),
     f(g(?y),h(?x)) = f(?y,?x) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <f(g(?x_3),g(?x)), f(?x_3,?x)> by Rules <0, 3> preceded by [(f,2)]
 joinable by a reduction of rules <[([(f,2)],1),([],3)], []>
Critical Pair <f(h(?x_1),h(?y_3)), f(?x_1,?y_3)> by Rules <1, 3> preceded by [(f,1)]
 joinable by a reduction of rules <[([],4)], [([],2)]>
Critical Pair <f(g(?x),h(?y_4)), f(?y_4,?x)> by Rules <0, 4> preceded by [(f,1)]
 joinable by a reduction of rules <[([],3)], [([],2)]>
Critical Pair <f(h(?x_4),g(?x)), f(?x,?x_4)> by Rules <0, 4> preceded by [(f,2)]
 joinable by a reduction of rules <[([(f,2)],1),([],4)], []>
 joinable by a reduction of rules <[([],2),([],3)], []>
Critical Pair <f(?x_3,?y_3), f(h(?y_3),g(?x_3))> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[], [([(f,2)],1),([],4)]>
 joinable by a reduction of rules <[], [([],2),([],3)]>
Critical Pair <f(?y_4,?x_4), f(h(?y_4),h(?x_4))> by Rules <4, 2> preceded by []
 joinable by a reduction of rules <[([],2)], [([],4)]>
Satisfiable by 1>4>3,5>2; f(1,1)g(0)h(0); 3>1>2>4>5
Diagram Decreasing
Direct Methods: CR

Combined result: CR
/tmp/filej6ZODG.trs: Success(CR)
(4 msec.)