Problem:
 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)

Proof:
 Church Rosser Transformation Processor (no redundant rules):
  strict:
   
  weak:
   
  critical peaks: 20
   f(v(x),y) <-0|[]- f(x,y) -1|[]-> f(x,u(y))
   f(v(v(x)),v(O())) <-0|[]- f(v(x),v(O())) -6|[]-> B()
   f(v(u(O())),u(y)) <-0|[]- f(u(O()),u(y)) -7|[]-> A()
   f(x,u(y)) <-1|[]- f(x,y) -0|[]-> f(v(x),y)
   f(v(x),u(v(O()))) <-1|[]- f(v(x),v(O())) -6|[]-> B()
   f(u(O()),u(u(y))) <-1|[]- f(u(O()),u(y)) -7|[]-> A()
   f(x,v(O())) <-2|0[]- f(v(x),v(O())) -6|[]-> B()
   f(v(x),O()) <-2|1[]- f(v(x),v(O())) -6|[]-> B()
   f(O(),u(y)) <-3|0[]- f(u(O()),u(y)) -7|[]-> A()
   f(u(O()),y) <-3|1[]- f(u(O()),u(y)) -7|[]-> A()
   v(O()) <-4|[]- O() -5|[]-> u(O())
   f(v(x),v(v(O()))) <-4|1,0[]- f(v(x),v(O())) -6|[]-> B()
   f(u(v(O())),u(y)) <-4|0,0[]- f(u(O()),u(y)) -7|[]-> A()
   u(O()) <-5|[]- O() -4|[]-> v(O())
   f(v(x),v(u(O()))) <-5|1,0[]- f(v(x),v(O())) -6|[]-> B()
   f(u(u(O())),u(y)) <-5|0,0[]- f(u(O()),u(y)) -7|[]-> A()
   B() <-6|[]- f(v(x130),v(O())) -0|[]-> f(v(v(x130)),v(O()))
   B() <-6|[]- f(v(x131),v(O())) -1|[]-> f(v(x131),u(v(O())))
   A() <-7|[]- f(u(O()),u(x132)) -0|[]-> f(v(u(O())),u(x132))
   A() <-7|[]- f(u(O()),u(x133)) -1|[]-> f(u(O()),u(u(x133)))
  Redundant Rules Transformation:
   f(x,y) -> f(v(x),y)
   f(x,y) -> f(x,u(y))
   v(x) -> x
   u(x) -> x
   O() -> v(O())
   O() -> u(O())
   f(v(x),v(O())) -> B()
   f(u(O()),u(y)) -> A()
   f(u(u(O())),u(y)) -> A()
   f(v(x),v(u(O()))) -> B()
   f(u(v(O())),u(y)) -> A()
   f(v(x),v(v(O()))) -> B()
   f(u(O()),y) -> A()
   f(O(),u(y)) -> A()
   f(v(x),O()) -> B()
   f(x,v(O())) -> B()
   f(v(x),u(v(O()))) -> B()
   f(v(u(O())),u(y)) -> A()
   f(v(u(O())),u(x132)) -> A()
   f(v(x131),u(v(O()))) -> B()
   Nonconfluence Processor:
    terms: B() *<- f(v(u(O())),u(v(O()))) ->* A()
    Qed
    
    first automaton:
     final states: {1}
     transitions:
      B() -> 1*
    
    second automaton:
     final states: {2}
     transitions:
      A() -> 2*