(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 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 by Rules <5, 0> preceded by [(f,2)]
joinable by a reduction of rules <[], []>
Critical Pair 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 by Rules <6, 1> preceded by [(f,1)]
joinable by a reduction of rules <[], []>
Critical Pair by Rules <5, 2> preceded by [(f,1)]
joinable by a reduction of rules <[([],3)], [([],4)]>
Critical Pair 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 by Rules <6, 3> preceded by [(f,1)]
joinable by a reduction of rules <[([],2)], [([],4)]>
Critical Pair 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 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 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 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 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.)