Problem:
 join(x,meet(x,y)) -> x
 meet(x,joint(y,z)) -> join(meet(x,y),meet(x,z))
 meet(x,x) -> x
 join(x,x) -> x
 meet(meet(x,y),z) -> meet(x,meet(y,z))
 meet(x,y) -> meet(y,x)
 join(join(x,y),z) -> join(x,join(y,z))
 join(x,y) -> join(y,x)

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 34
   join(x,y) <-0|[]- join(join(x,y),meet(join(x,y),x208)) -6|[]-> join
                                                                  (x,join(y,meet(join(x,y),x208)))
   join(x,z) <-0|0[]- join(join(x,meet(x,x210)),z) -6|[]-> join(x,join(meet(x,x210),z))
   x <-0|[]- join(x,meet(x,x212)) -7|[]-> join(meet(x,x212),x)
   join(x,join(meet(x,x214),meet(x,x215))) <-1|1[]- join(x,meet(x,joint(x214,x215))) -0|[]-> x
   join(meet(joint(x217,x218),x217),meet(joint(x217,x218),x218)) <-1|
   []- meet(joint(x217,x218),joint(x217,x218)) -2|[]-> joint(x217,x218)
   join(meet(meet(x,y),x220),meet(meet(x,y),x221)) <-1|[]- meet(meet(x,y),joint(x220,x221)) -4|
                                                           []-> meet(x,meet(y,joint(x220,x221)))
   meet(join(meet(x,x223),meet(x,x224)),z) <-1|0[]- meet(meet(x,joint(x223,x224)),z) -4|
                                                    []-> meet(x,meet(joint(x223,x224),z))
   join(meet(x,x226),meet(x,x227)) <-1|[]- meet(x,joint(x226,x227)) -5|
                                           []-> meet(joint(x226,x227),x)
   join(y,y) <-2|1[]- join(y,meet(y,y)) -0|[]-> y
   joint(y,z) <-2|[]- meet(joint(y,z),joint(y,z)) -1|[]-> join(meet(joint(y,z),y),
                                                               meet(joint(y,z),z))
   meet(x,y) <-2|[]- meet(meet(x,y),meet(x,y)) -4|[]-> meet(x,meet(y,meet(x,y)))
   meet(y,z) <-2|0[]- meet(meet(y,y),z) -4|[]-> meet(y,meet(y,z))
   y <-2|[]- meet(y,y) -5|[]-> meet(y,y)
   join(x,y) <-3|[]- join(join(x,y),join(x,y)) -6|[]-> join(x,join(y,join(x,y)))
   join(y,z) <-3|0[]- join(join(y,y),z) -6|[]-> join(y,join(y,z))
   y <-3|[]- join(y,y) -7|[]-> join(y,y)
   join(meet(x236,x237),meet(x236,meet(x237,y))) <-4|1[]- join(meet(x236,x237),
                                                               meet(meet(x236,x237),y)) -0|
                                                          []-> meet(x236,x237)
   meet(x239,meet(x240,joint(y,z))) <-4|[]- meet(meet(x239,x240),joint(y,z)) -1|
                                            []-> join(meet(meet(x239,x240),y),
                                                      meet(meet(x239,x240),z))
   meet(x242,meet(x243,meet(x242,x243))) <-4|[]- meet(meet(x242,x243),meet(x242,x243)) -2|
                                                 []-> meet(x242,x243)
   meet(meet(x245,meet(x246,y)),z) <-4|0[]- meet(meet(meet(x245,x246),y),z) -4|
                                            []-> meet(meet(x245,x246),meet(y,z))
   meet(x248,meet(x249,y)) <-4|[]- meet(meet(x248,x249),y) -5|[]-> meet(y,meet(x248,x249))
   join(x,meet(y,x)) <-5|1[]- join(x,meet(x,y)) -0|[]-> x
   meet(joint(y,z),x) <-5|[]- meet(x,joint(y,z)) -1|[]-> join(meet(x,y),meet(x,z))
   meet(x,x) <-5|[]- meet(x,x) -2|[]-> x
   meet(z,meet(x,y)) <-5|[]- meet(meet(x,y),z) -4|[]-> meet(x,meet(y,z))
   meet(meet(y,x),z) <-5|0[]- meet(meet(x,y),z) -4|[]-> meet(x,meet(y,z))
   join(x261,join(x262,meet(join(x261,x262),y))) <-6|[]- join(join(x261,x262),
                                                              meet(join(x261,x262),y)) -0|
                                                         []-> join(x261,x262)
   join(x264,join(x265,join(x264,x265))) <-6|[]- join(join(x264,x265),join(x264,x265)) -3|
                                                 []-> join(x264,x265)
   join(join(x267,join(x268,y)),z) <-6|0[]- join(join(join(x267,x268),y),z) -6|
                                            []-> join(join(x267,x268),join(y,z))
   join(x270,join(x271,y)) <-6|[]- join(join(x270,x271),y) -7|[]-> join(y,join(x270,x271))
   join(meet(x,y),x) <-7|[]- join(x,meet(x,y)) -0|[]-> x
   join(x,x) <-7|[]- join(x,x) -3|[]-> x
   join(z,join(x,y)) <-7|[]- join(join(x,y),z) -6|[]-> join(x,join(y,z))
   join(join(y,x),z) <-7|0[]- join(join(x,y),z) -6|[]-> join(x,join(y,z))
  Redundant Rules Transformation:
   join(x,meet(x,y)) -> x
   meet(x,joint(y,z)) -> join(meet(x,y),meet(x,z))
   meet(x,x) -> x
   join(x,x) -> x
   meet(meet(x,y),z) -> meet(x,meet(y,z))
   meet(x,y) -> meet(y,x)
   join(join(x,y),z) -> join(x,join(y,z))
   join(x,y) -> join(y,x)
   meet(y,x) -> meet(y,x)
   join(meet(x,y),x) -> x
   join(y,x) -> join(y,x)
   join(y,meet(x,y)) -> y
   join(meet(y,x282),y) -> y
   meet(meet(x,x),x) -> x
   meet(x,meet(x,x)) -> x
   meet(join(x,x),x) -> x
   meet(x,join(x,x)) -> x
   join(meet(x,x),x) -> x
   join(x,meet(x,x)) -> x
   join(join(x,x),x) -> x
   join(x,join(x,x)) -> x
   meet(x,y) -> meet(x,y)
   join(x,y) -> join(x,y)
   Nonconfluence Processor:
    terms: join(joint(f25(),f26()),join(meet(f3(),f25()),meet(f3(),f26()))) *<- 
    join(joint(f25(),f26()),meet(f3(),joint(f25(),f26()))) ->* joint(f25(),f26())
    Qed
    
    first automaton:
     final states: {992}
     transitions:
      f26() -> 2944*,1000,993
      f3() -> 2945*,997,994
      meet(2945,996) -> 998*
      meet(2946,997) -> 998*
      meet(996,2945) -> 998*
      meet(996,997) -> 998*
      meet(993,994) -> 995*
      meet(994,993) -> 995*
      meet(2945,993) -> 995*
      meet(2945,2946) -> 998*
      meet(2944,994) -> 995*
      meet(993,2945) -> 995*
      meet(2945,2944) -> 995*
      meet(997,996) -> 998*
      meet(994,2944) -> 995*
      meet(997,2946) -> 998*
      meet(2946,2945) -> 998*
      meet(2944,2945) -> 995*
      join(995,1002) -> 23310*
      join(998,1002) -> 24971*
      join(998,995) -> 999*
      join(1002,995) -> 23310*
      join(998,23310) -> 992*
      join(995,998) -> 999*
      join(995,24971) -> 992*
      join(23310,998) -> 992*
      join(1002,998) -> 24971*
      join(24971,995) -> 992*
      join(1002,999) -> 992*
      join(999,1002) -> 992*
      joint(2946,1000) -> 1002*
      joint(1001,2944) -> 1002*
      joint(2946,2944) -> 1002*
      joint(1001,1000) -> 1002*
      f25() -> 2946*,1001,996
    
    second automaton:
     final states: {1003}
     transitions:
      f26() -> 1004*
      joint(1005,1004) -> 1003*
      f25() -> 1005*