NO
(ignored inputs)COMMENT Example 4 from [F12-IWC]. not confluent.
Rewrite Rules:
   [ f(u(O),u(?y)) -> A,
     f(v(?x),v(O)) -> B,
     O -> u(O),
     O -> v(O),
     u(?x) -> ?x,
     v(?x) -> ?x,
     f(?x,?y) -> f(?x,u(?y)),
     f(?x,?y) -> f(v(?x),?y) ]
Apply Direct Methods...
Inner CPs:
   [ f(u(u(O)),u(?y)) = A,
     f(u(v(O)),u(?y)) = A,
     f(O,u(?y)) = A,
     f(u(O),?x_2) = A,
     f(v(?x_1),v(u(O))) = B,
     f(v(?x_1),v(v(O))) = B,
     f(?x_3,v(O)) = B,
     f(v(?x_1),O) = B ]
Outer CPs:
   [ A = f(u(O),u(u(?y))),
     A = f(v(u(O)),u(?y)),
     B = f(v(?x_1),u(v(O))),
     B = f(v(v(?x_1)),v(O)),
     u(O) = v(O),
     f(?x_4,u(?y_4)) = f(v(?x_4),?y_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(u(O),u(?y)) = A,
     f(v(O),u(?y)) = A,
     f(v(u(O)),?y) = A,
     f(v(v(O)),?y) = A,
     f(u(O),u(u(?y))) = A,
     f(v(O),u(u(?y))) = A,
     f(O,u(?y)) = A,
     f(u(u(O)),u(?y)) = A,
     f(u(v(O)),u(?y)) = A,
     f(v(u(O)),u(?y)) = A,
     f(v(v(O)),u(?y)) = A,
     f(v(O),?y) = A,
     f(v(u(u(O))),?y) = A,
     f(v(u(v(O))),?y) = A,
     f(u(O),?y) = A,
     f(O,u(u(?y))) = A,
     f(u(u(O)),u(u(?y))) = A,
     f(u(v(O)),u(u(?y))) = A,
     f(v(u(u(O))),u(?y)) = A,
     f(v(u(v(O))),u(?y)) = A,
     f(O,?y) = A,
     f(u(u(O)),?y) = A,
     f(u(v(O)),?y) = A,
     f(?x,u(u(O))) = B,
     f(?x,u(v(O))) = B,
     f(v(?x),u(O)) = B,
     f(v(?x),v(O)) = B,
     f(?x,u(O)) = B,
     f(?x,u(v(u(O)))) = B,
     f(?x,u(v(v(O)))) = B,
     f(v(?x),u(u(O))) = B,
     f(v(?x),u(v(O))) = B,
     f(v(?x),O) = B,
     f(v(?x),v(u(O))) = B,
     f(v(?x),v(v(O))) = B,
     f(v(v(?x)),u(O)) = B,
     f(v(v(?x)),v(O)) = B,
     f(?x,v(O)) = B,
     f(v(?x),u(v(u(O)))) = B,
     f(v(?x),u(v(v(O)))) = B,
     f(v(v(?x)),O) = B,
     f(v(v(?x)),v(u(O))) = B,
     f(v(v(?x)),v(v(O))) = B,
     f(?x,O) = B,
     f(?x,v(u(O))) = B,
     f(?x,v(v(O))) = B,
     v(O) = u(O),
     A = f(u(u(O)),u(?y)),
     B = f(v(?x_1),v(u(O))),
     u(O) = v(O),
     A = f(u(v(O)),u(?y)),
     B = f(v(?x_1),v(v(O))),
     A = f(O,u(?y_2)),
     A = f(u(O),?x),
     B = f(?x,v(O)),
     B = f(v(?x_3),O),
     A = f(u(O),u(u(?y_1))),
     B = f(v(?x_2),u(v(O))),
     f(v(?x),?y) = f(?x,u(?y)),
     A = f(v(u(O)),u(?y_1)),
     B = f(v(v(?x_2)),v(O)),
     f(?x,u(?y)) = f(v(?x),?y) ]
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(u(u(O)),u(?y)), A> by Rules <2, 0> preceded by [(f,1),(u,1)]
 joinable by a reduction of rules <[([(f,1),(u,1)],4),([],0)], []>
 joinable by a reduction of rules <[([(f,1)],4),([],0)], []>
Critical Pair <f(u(v(O)),u(?y)), A> by Rules <3, 0> preceded by [(f,1),(u,1)]
 joinable by a reduction of rules <[([(f,1),(u,1)],5),([],0)], []>
Critical Pair <f(O,u(?y)), A> by Rules <4, 0> preceded by [(f,1)]
 joinable by a reduction of rules <[([(f,1)],2),([],0)], []>
Critical Pair <f(u(O),?x_2), A> by Rules <4, 0> preceded by [(f,2)]
 joinable by a reduction of rules <[([],6),([],0)], []>
Critical Pair <f(v(?x_1),v(u(O))), B> by Rules <2, 1> preceded by [(f,2),(v,1)]
 joinable by a reduction of rules <[([(f,2),(v,1)],4),([],1)], []>
Critical Pair <f(v(?x_1),v(v(O))), B> by Rules <3, 1> preceded by [(f,2),(v,1)]
 joinable by a reduction of rules <[([(f,2),(v,1)],5),([],1)], []>
 joinable by a reduction of rules <[([(f,2)],5),([],1)], []>
Critical Pair <f(?x_3,v(O)), B> by Rules <5, 1> preceded by [(f,1)]
 joinable by a reduction of rules <[([],7),([],1)], []>
Critical Pair <f(v(?x_1),O), B> by Rules <5, 1> preceded by [(f,2)]
 joinable by a reduction of rules <[([(f,2)],3),([],1)], []>
Critical Pair <f(u(O),u(u(?y))), A> by Rules <6, 0> preceded by []
 joinable by a reduction of rules <[([],0)], []>
Critical Pair <f(v(u(O)),u(?y)), A> by Rules <7, 0> preceded by []
 joinable by a reduction of rules <[([(f,1)],5),([],0)], []>
Critical Pair <f(v(?x_1),u(v(O))), B> by Rules <6, 1> preceded by []
 joinable by a reduction of rules <[([(f,2)],4),([],1)], []>
Critical Pair <f(v(v(?x_1)),v(O)), B> by Rules <7, 1> preceded by []
 joinable by a reduction of rules <[([],1)], []>
Critical Pair <v(O), u(O)> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[([],5)], [([],4)]>
Critical Pair <f(v(?x_5),?y_5), f(?x_5,u(?y_5))> by Rules <7, 6> preceded by []
 joinable by a reduction of rules <[([(f,1)],5)], [([(f,2)],4)]>
 joinable by a reduction of rules <[([],6)], [([],7)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 18 rules by 3 steps unfolding
strenghten u(O) and O
strenghten v(O) and O
strenghten u(O) and v(O)
strenghten v(O) and u(O)
strenghten u(u(O)) and O
strenghten u(v(O)) and O
strenghten v(u(O)) and O
strenghten v(v(O)) and O
strenghten u(u(O)) and u(O)
strenghten u(u(O)) and v(O)
strenghten u(v(O)) and u(O)
strenghten u(v(O)) and v(O)
strenghten v(u(O)) and u(O)
strenghten v(u(O)) and v(O)
strenghten f(?x_3,v(O)) and B
strenghten f(O,u(?y)) and A
strenghten f(O,v(O)) and B
strenghten f(u(O),?x_2) and A
strenghten f(u(O),O) and A
strenghten f(v(?x_1),O) and B
strenghten u(u(u(O))) and O
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (success)
Witness for Non-Confluence: <A, B>
Direct Methods: not CR

Final result: not CR
216.trs: Success(not CR)
(28 msec.)