(ignored inputs)COMMENT R8 of \cite{AT2012}
Rewrite Rules:
   [ f(g(?x),g(?y)) -> f(g(?x),h(?y)),
     f(h(?x),g(?y)) -> f(g(?x),g(?y)),
     f(g(?x),h(?y)) -> f(?x,?y),
     f(h(?x),h(?y)) -> f(?y,?x),
     f(?x,?y) -> f(?y,?x),
     g(?x) -> h(?x),
     h(?x) -> g(?x) ]
Apply Direct Methods...
Inner CPs:
   [ f(h(?x_5),g(?y)) = f(g(?x_5),h(?y)),
     f(g(?x),h(?x_5)) = f(g(?x),h(?x_5)),
     f(h(?x_1),h(?x_5)) = f(g(?x_1),g(?x_5)),
     f(g(?x_6),g(?y_1)) = f(g(?x_6),g(?y_1)),
     f(h(?x_5),h(?y_2)) = f(?x_5,?y_2),
     f(g(?x_2),g(?x_6)) = f(?x_2,?x_6),
     f(g(?x_6),h(?y_3)) = f(?y_3,?x_6),
     f(h(?x_3),g(?x_6)) = f(?x_6,?x_3) ]
Outer CPs:
   [ f(g(?x),h(?y)) = f(g(?y),g(?x)),
     f(g(?x_1),g(?y_1)) = f(g(?y_1),h(?x_1)),
     f(?x_2,?y_2) = f(h(?y_2),g(?x_2)),
     f(?y_3,?x_3) = f(h(?y_3),h(?x_3)) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth&Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ f(?y_5,?x) = f(g(?x),h(?y_5)),
     f(?x_4,?x) = f(g(?x_4),g(?x)),
     f(g(?x_3),g(?x)) = f(h(?x_3),h(?x)),
     f(g(?x),h(?y_2)) = f(h(?x),g(?y_2)),
     f(?y_4,?x_4) = f(h(?y_4),h(?x_4)),
     f(?x_3,?y_3) = f(h(?y_3),g(?x_3)),
     f(g(?y),h(?x)) = f(?y,?x),
     f(g(?x),g(?y)) = f(?x,?y),
     f(h(?x),h(?y)) = f(?x,?y),
     f(h(?y),g(?x)) = f(?x,?y),
     f(h(?x),g(?y)) = f(?x,?y),
     f(g(?y),g(?x)) = f(?x,?y),
     f(h(?y),h(?x)) = f(?x,?y),
     f(g(?y),h(?x)) = f(?x,?y),
     f(h(?x),h(?y)) = f(g(?x),g(?y)),
     f(g(?x),g(?y)) = f(g(?x),g(?y)),
     f(g(?y),h(?x)) = f(g(?x),g(?y)),
     f(g(?x),h(?y)) = f(g(?x),g(?y)),
     f(h(?y),h(?x)) = f(g(?x),g(?y)),
     f(g(?y),g(?x)) = f(g(?x),g(?y)),
     f(h(?y),g(?x)) = f(g(?x),g(?y)),
     f(g(?x),h(?y)) = f(g(?x),h(?y)),
     f(h(?x),g(?y)) = f(g(?x),h(?y)),
     f(g(?y),g(?x)) = f(g(?x),h(?y)),
     f(h(?x),h(?y)) = f(g(?x),h(?y)),
     f(h(?y),g(?x)) = f(g(?x),h(?y)),
     f(g(?y),h(?x)) = f(g(?x),h(?y)),
     f(h(?y),h(?x)) = f(g(?x),h(?y)) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <f(h(?x_5),g(?y)), f(g(?x_5),h(?y))> by Rules <5, 0> preceded by [(f,1)]
 joinable by a reduction of rules <[([(f,2)],5)], [([(f,1)],5)]>
 joinable by a reduction of rules <[([(f,1)],6)], [([(f,2)],6)]>
 joinable by a reduction of rules <[([],1)], [([(f,2)],6)]>
Critical Pair <f(g(?x),h(?x_5)), f(g(?x),h(?x_5))> by Rules <5, 0> preceded by [(f,2)]
 joinable by a reduction of rules <[], []>
Critical Pair <f(h(?x_1),h(?x_5)), f(g(?x_1),g(?x_5))> by Rules <5, 1> preceded by [(f,2)]
 joinable by a reduction of rules <[([(f,2)],6)], [([(f,1)],5)]>
 joinable by a reduction of rules <[([(f,1)],6)], [([(f,2)],5)]>
 joinable by a reduction of rules <[([(f,1)],6)], [([],0)]>
Critical Pair <f(g(?x_6),g(?y_1)), f(g(?x_6),g(?y_1))> by Rules <6, 1> preceded by [(f,1)]
 joinable by a reduction of rules <[], []>
Critical Pair <f(h(?x_5),h(?y_2)), f(?x_5,?y_2)> by Rules <5, 2> preceded by [(f,1)]
 joinable by a reduction of rules <[([],3)], [([],4)]>
Critical Pair <f(g(?x_2),g(?x_6)), f(?x_2,?x_6)> by Rules <6, 2> preceded by [(f,2)]
 joinable by a reduction of rules <[([(f,2)],5),([],2)], []>
 joinable by a reduction of rules <[([],0),([],2)], []>
Critical Pair <f(g(?x_6),h(?y_3)), f(?y_3,?x_6)> by Rules <6, 3> preceded by [(f,1)]
 joinable by a reduction of rules <[([],2)], [([],4)]>
Critical Pair <f(h(?x_3),g(?x_6)), f(?x_6,?x_3)> by Rules <6, 3> preceded by [(f,2)]
 joinable by a reduction of rules <[([(f,2)],5),([],3)], []>
 joinable by a reduction of rules <[([],4),([],2)], []>
Critical Pair <f(g(?y),g(?x)), f(g(?x),h(?y))> by Rules <4, 0> preceded by []
 joinable by a reduction of rules <[([(f,1)],5)], [([],4)]>
 joinable by a reduction of rules <[([],4)], [([(f,2)],6)]>
Critical Pair <f(g(?y_1),h(?x_1)), f(g(?x_1),g(?y_1))> by Rules <4, 1> preceded by []
 joinable by a reduction of rules <[([(f,2)],6)], [([],4)]>
 joinable by a reduction of rules <[([],4)], [([(f,1)],5)]>
Critical Pair <f(h(?y_2),g(?x_2)), f(?x_2,?y_2)> by Rules <4, 2> preceded by []
 joinable by a reduction of rules <[([(f,2)],5),([],3)], []>
 joinable by a reduction of rules <[([],4),([],2)], []>
Critical Pair <f(h(?y_3),h(?x_3)), f(?y_3,?x_3)> by Rules <4, 3> preceded by []
 joinable by a reduction of rules <[([],3)], [([],4)]>
Satisfiable by 2>4,3>5>1>7>6; f(1,1)g(0)h(0); 2>5>1>7>3,4>6
Diagram Decreasing
Direct Methods: CR

Final result: CR
/local-scratch/hzankl/2012/cops2012/121.trs: Success(CR)
(8 msec.)