(ignored inputs)COMMENT Example 3.2 of \cite{KS10} doi: http://dx.doi.org/10.1007/978-3-642-12251-4_20 Rewrite Rules: [ a -> b, a -> c, a -> e, b -> d, c -> a, d -> a, d -> e, g(?x) -> h(a), h(?x) -> e ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ b = c, b = e, c = e, a = e ] Overlay, check Innermost Termination... unknown Innermost 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: [ a = e, e = a, c = e, b = e, e = c, b = c, e = b, c = b ] unknown Okui (Simultaneous CPs) unknown Strongly Depth-Preserving & Non-E-Overlapping check Locally Decreasing Diagrams by Rule Labelling... Critical Pair by Rules <1, 0> preceded by [] joinable by a reduction of rules <[([],4),([],0)], []> joinable by a reduction of rules <[([],4)], [([],3),([],5)]> joinable by a reduction of rules <[([],4),([],2)], [([],3),([],6)]> Critical Pair by Rules <2, 0> preceded by [] joinable by a reduction of rules <[], [([],3),([],6)]> Critical Pair by Rules <2, 1> preceded by [] joinable by a reduction of rules <[], [([],4),([],2)]> Critical Pair by Rules <6, 5> preceded by [] joinable by a reduction of rules <[], [([],2)]> Satisfiable by 1>6>2,3,5,7>4,8,9; g(0)h(0); 2>1>6>3,5,7>4,8,9 Diagram Decreasing Direct Methods: CR Final result: CR /local-scratch/hzankl/2012/cops2012/111.trs: Success(CR) (21 msec.)