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:
  strict:
   
  weak:
   
  critical peaks: 20
   A() <-0|[]- f(u(O()),u(x114)) -6|[]-> f(u(O()),u(u(x114)))
   A() <-0|[]- f(u(O()),u(x115)) -7|[]-> f(v(u(O())),u(x115))
   B() <-1|[]- f(v(x116),v(O())) -6|[]-> f(v(x116),u(v(O())))
   B() <-1|[]- f(v(x117),v(O())) -7|[]-> f(v(v(x117)),v(O()))
   f(u(u(O())),u(y)) <-2|0,0[]- f(u(O()),u(y)) -0|[]-> A()
   f(v(x),v(u(O()))) <-2|1,0[]- f(v(x),v(O())) -1|[]-> B()
   u(O()) <-2|[]- O() -3|[]-> v(O())
   f(u(v(O())),u(y)) <-3|0,0[]- f(u(O()),u(y)) -0|[]-> A()
   f(v(x),v(v(O()))) <-3|1,0[]- f(v(x),v(O())) -1|[]-> B()
   v(O()) <-3|[]- O() -2|[]-> u(O())
   f(O(),u(y)) <-4|0[]- f(u(O()),u(y)) -0|[]-> A()
   f(u(O()),y) <-4|1[]- f(u(O()),u(y)) -0|[]-> A()
   f(x,v(O())) <-5|0[]- f(v(x),v(O())) -1|[]-> B()
   f(v(x),O()) <-5|1[]- f(v(x),v(O())) -1|[]-> B()
   f(u(O()),u(u(y))) <-6|[]- f(u(O()),u(y)) -0|[]-> A()
   f(v(x),u(v(O()))) <-6|[]- f(v(x),v(O())) -1|[]-> B()
   f(x,u(y)) <-6|[]- f(x,y) -7|[]-> f(v(x),y)
   f(v(u(O())),u(y)) <-7|[]- f(u(O()),u(y)) -0|[]-> A()
   f(v(v(x)),v(O())) <-7|[]- f(v(x),v(O())) -1|[]-> B()
   f(v(x),y) <-7|[]- f(x,y) -6|[]-> f(x,u(y))
  Redundant Rules Transformation:
   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)
   O() -> u(u(O()))
   O() -> u(v(O()))
   O() -> O()
   O() -> v(u(O()))
   O() -> v(v(O()))
   u(f(u(O()),u(y))) -> A()
   u(f(v(x),v(O()))) -> B()
   u(O()) -> u(O())
   u(O()) -> v(O())
   u(u(x)) -> x
   u(v(x)) -> x
   v(f(u(O()),u(y))) -> A()
   v(f(v(x),v(O()))) -> B()
   v(O()) -> u(O())
   v(O()) -> v(O())
   v(u(x)) -> x
   v(v(x)) -> x
   f(u(O()),y) -> A()
   f(x146,x) -> f(x146,x)
   f(x,v(O())) -> B()
   f(x,x149) -> f(x,x149)
   f(O(),u(x134)) -> A()
   f(u(O()),O()) -> A()
   f(u(O()),u(O())) -> A()
   u(f(u(O()),u(x134))) -> A()
   f(u(u(O())),u(x134)) -> A()
   f(u(O()),u(u(x134))) -> A()
   f(u(O()),u(u(x))) -> A()
   v(f(u(O()),u(x134))) -> A()
   f(v(u(O())),u(x134)) -> A()
   f(u(v(O())),u(x134)) -> A()
   f(u(O()),v(u(x134))) -> A()
   f(u(O()),u(v(x))) -> A()
   f(v(O()),v(O())) -> B()
   f(O(),v(O())) -> B()
   f(v(x135),O()) -> B()
   u(f(v(x135),v(O()))) -> B()
   f(u(v(x135)),v(O())) -> B()
   f(v(u(x)),v(O())) -> B()
   f(v(x135),u(v(O()))) -> B()
   f(v(x135),v(u(O()))) -> B()
   v(f(v(x135),v(O()))) -> B()
   f(v(v(x135)),v(O())) -> B()
   f(v(v(x)),v(O())) -> B()
   f(v(x135),v(v(O()))) -> B()
   u(u(x136)) -> x136
   v(u(x136)) -> x136
   u(v(x137)) -> x137
   v(v(x137)) -> x137
   Nonconfluence Processor:
    terms: A() *<- f(u(O()),v(O())) ->* B()
    Qed