(ignored inputs)COMMENT Example 8 from [HM11]: doi: http://dx.doi.org/10.1007/s10817-011-9238-x
Rewrite Rules:
   [ f(a,a) -> c,
     f(b,?x) -> f(?x,?x),
     f(?x,b) -> f(?x,?x),
     a -> b ]
Apply Direct Methods...
Inner CPs:
   [ f(b,a) = c,
     f(a,b) = c ]
Outer CPs:
   [ f(b,b) = f(b,b) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth&Bendix
Left-Linear, not Right-Linear
unknown Development Closed
inner CP cond (upside-parallel)
innter CP Cond (outside)
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ c = f(a,b),
     c = f(b,a),
     f(b,b) = f(b,b),
     f(a,b) = c,
     f(b,a) = c,
     f(b,b) = c ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <f(b,a), c> by Rules <3, 0> preceded by [(f,1)]
 joinable by a reduction of rules <[([],1),([],0)], []>
Critical Pair <f(a,b), c> by Rules <3, 0> preceded by [(f,2)]
 joinable by a reduction of rules <[([],2),([],0)], []>
Critical Pair <f(b,b), f(b,b)> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[], []>
unknown Diagram Decreasing
check by Reduction-Preserving Completion...
failure(empty P)
unknown Reduction-Preserving Completion
check Non-Confluence...Find Non-Joinable CP reducts: <f(b,b), c> from f(a,a)
Not Confluent
Direct Methods: not CR

Final result: not CR
/local-scratch/hzankl/2012/cops2012/113.trs: Success(not CR)
(15 msec.)