---- CR(R)
---- [Jouannaud and Kirchner, 1986]
R:
join(x,meet(x,y)) -> x
meet(x,join(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)
CP_AC(R):
meet(x,join(y,z)) -> join(meet(x,join(y,meet(join(y,z),w))),meet(x,z))
meet(x,y) -> join(meet(x,y,z),meet(x,y))
meet(x,join(y,z)) -> join(meet(x,y),meet(x,join(z,meet(join(y,z),w))))
meet(x,y) -> join(meet(x,y),meet(x,y,z))
join(meet(x,join(y,z)),meet(x,w,y),meet(x,w,z)) -> meet(x,join(y,z))
join(x,y,meet(z,x),meet(z,y)) -> join(x,y)
join(x,meet(x,y,z),meet(x,y,w)) -> x
join(x,meet(x,y),meet(x,z)) -> x
join(meet(x,x,join(y,z),y),meet(x,x,join(y,z),z)) -> meet(x,join(y,z))
join(meet(join(x,y),x),meet(join(x,y),y)) -> join(x,y)
join(meet(x,x),meet(x,y)) -> meet(x,x)
join(meet(x,x,y),meet(x,y,z)) -> meet(x,x,y)
join(x,meet(x,y)) -> x
join(meet(x,x,y),meet(x,y)) -> meet(x,x,y)
join(x,x) -> x
meet(x,join(y,z)) -> join(meet(x,x,join(y,z),y),meet(x,x,join(y,z),z))
join(x,y) -> join(meet(join(x,y),x),meet(join(x,y),y))
meet(x,join(y,z)) -> join(meet(x,join(y,y)),meet(x,join(z,z)))
meet(x,join(y,z,w)) -> join(meet(x,join(y,y,z)),meet(x,join(z,w,w)))
meet(x,join(y,z)) -> join(meet(x,y),meet(x,join(y,z,z)))
meet(x,join(y,z)) -> join(meet(x,join(y,y,z)),meet(x,z))
meet(x,y) -> join(meet(x,y),meet(x,y))
join(x,y) -> join(y,x,meet(join(x,y),z))
x -> join(x,meet(x,y))
join(x,y) -> join(y,meet(join(x,y),z),x)
x -> join(meet(x,y),x)
join(x,y,z) -> join(x,meet(join(x,y,z),w),y,z)
join(x,y) -> join(meet(join(x,y),z),x,y)
join(x,y,z) -> join(x,y,meet(join(x,y,z),w),z)
join(x,y) -> join(x,meet(join(x,y),z),y)
join(x,y,z) -> join(x,y,z,meet(join(x,y,z),w))
join(x,y) -> join(x,y,meet(join(x,y),z))
join(x,y,z) -> join(x,meet(join(x,y),w),y,z)
join(x,y) -> join(meet(x,z),x,y)
join(x,y,z) -> join(x,y,meet(join(x,y),w),z)
join(x,y) -> join(x,meet(x,z),y)
join(x,y,z) -> join(x,meet(join(x,y,z),w),y,z)
join(x,y) -> join(meet(join(x,y),z),x,y)
join(x,y,z) -> join(x,y,meet(join(x,y,z),w),z)
join(x,y) -> join(x,meet(join(x,y),z),y)
join(x,y,z) -> join(x,y,z,meet(join(x,y,z),w))
join(x,y) -> join(x,y,meet(join(x,y),z))
join(x,y,z) -> join(x,y,meet(join(y,z),w),z)
join(x,y) -> join(x,meet(y,z),y)
join(x,y,z) -> join(x,y,z,meet(join(y,z),w))
join(x,y) -> join(x,y,meet(y,z))
join(meet(x,y,z),meet(x,y,w)) -> meet(y,x,join(z,w))
join(meet(x,y),meet(x,z)) -> meet(x,join(y,z))
join(meet(x,y,z),meet(x,y,w)) -> meet(y,join(z,w),x)
join(meet(x,y),meet(x,z)) -> meet(join(y,z),x)
join(meet(x,y,z,w),meet(x,y,z,x1)) -> meet(x,join(w,x1),y,z)
join(meet(x,y,z),meet(x,y,w)) -> meet(join(z,w),x,y)
join(meet(x,y,z,w),meet(x,y,z,x1)) -> meet(x,y,join(w,x1),z)
join(meet(x,y,z),meet(x,y,w)) -> meet(x,join(z,w),y)
join(meet(x,y,z,w),meet(x,y,z,x1)) -> meet(x,y,z,join(w,x1))
join(meet(x,y,z),meet(x,y,w)) -> meet(x,y,join(z,w))
meet(join(meet(x,y,z),meet(x,y,w)),x1) -> meet(x,join(z,w),y,x1)
meet(join(meet(x,y),meet(x,z)),w) -> meet(join(y,z),x,w)
meet(join(meet(x,y,z),meet(x,y,w)),x1) -> meet(x,y,join(z,w),x1)
meet(join(meet(x,y),meet(x,z)),w) -> meet(x,join(y,z),w)
join(meet(x,y,z,w),meet(x,y,z,x1)) -> meet(x,join(w,x1),y,z)
join(meet(x,y,z),meet(x,y,w)) -> meet(join(z,w),x,y)
join(meet(x,y,z,w),meet(x,y,z,x1)) -> meet(x,y,join(w,x1),z)
join(meet(x,y,z),meet(x,y,w)) -> meet(x,join(z,w),y)
join(meet(x,y,z,w),meet(x,y,z,x1)) -> meet(x,y,z,join(w,x1))
join(meet(x,y,z),meet(x,y,w)) -> meet(x,y,join(z,w))
meet(x,join(meet(y,z,w),meet(y,z,x1))) -> meet(x,y,join(w,x1),z)
meet(x,join(meet(y,z),meet(y,w))) -> meet(x,join(z,w),y)
meet(x,join(meet(y,z,w),meet(y,z,x1))) -> meet(x,y,z,join(w,x1))
meet(x,join(meet(y,z),meet(y,w))) -> meet(x,y,join(z,w))
meet(x,y) -> meet(y,y,x,x)
meet(x,y,z) -> meet(y,z,z,x,x,y)
meet(x,y) -> meet(x,y,y,x)
meet(x,y) -> meet(y,x,x,y)
x -> meet(x,x)
meet(x,y,z) -> meet(x,x,y,z,y,z)
meet(x,y) -> meet(x,y,x,y)
meet(x,y,z,w) -> meet(x,x,y,z,y,w,z,w)
meet(x,y,z) -> meet(x,y,x,z,y,z)
meet(x,y) -> meet(x,x,y,y)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y) -> meet(x,x,y,y)
meet(x,y,z,w) -> meet(x,x,y,z,z,w,y,w)
meet(x,y,z) -> meet(x,y,y,z,x,z)
meet(x,y,z,w,x1) -> meet(x,x,y,z,y,w,w,x1,z,x1)
meet(x,y,z,w) -> meet(x,y,x,z,z,w,y,w)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y,z,w) -> meet(x,x,y,y,z,z,w,w)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y,z) -> meet(x,x,y,z,y,z)
meet(x,y) -> meet(x,y,x,y)
meet(x,y,z) -> meet(x,x,y,z,z,y)
meet(x,y) -> meet(x,y,y,x)
meet(x,y,z,w) -> meet(x,x,y,z,y,w,w,z)
meet(x,y,z) -> meet(x,y,x,z,z,y)
meet(x,y,z,w) -> meet(x,x,y,z,y,z,w,w)
meet(x,y,z) -> meet(x,y,x,y,z,z)
meet(x,y,z,w,x1) -> meet(x,x,y,z,y,w,z,w,x1,x1)
meet(x,y,z,w) -> meet(x,y,x,z,y,z,w,w)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y,z,w) -> meet(x,x,y,y,z,z,w,w)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y,z,w,x1) -> meet(x,x,y,z,z,w,y,w,x1,x1)
meet(x,y,z,w) -> meet(x,y,y,z,x,z,w,w)
meet(x,y,z,w,x1,x2) -> meet(x,x,y,z,y,w,w,x1,z,x1,x2,x2)
meet(x,y,z,w,x1) -> meet(x,y,x,z,z,w,y,w,x1,x1)
meet(x,y,z,w) -> meet(x,x,y,y,z,z,w,w)
meet(x,y,z,w,x1) -> meet(x,x,y,y,z,z,w,w,x1,x1)
meet(x,y,z,w) -> meet(x,x,y,y,z,z,w,w)
meet(x,y,z,w) -> meet(x,x,y,z,y,z,w,w)
meet(x,y,z) -> meet(x,y,x,y,z,z)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y) -> meet(x,x,y,y)
meet(x,y,z,w) -> meet(x,x,y,z,z,y,w,w)
meet(x,y,z) -> meet(x,y,y,x,z,z)
meet(x,y,z,w,x1) -> meet(x,x,y,z,y,w,w,z,x1,x1)
meet(x,y,z,w) -> meet(x,y,x,z,z,y,w,w)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y,z,w) -> meet(x,x,y,y,z,z,w,w)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y,z) -> meet(x,x,y,y,z)
meet(x,y,z,w) -> meet(x,x,y,y,z,z,w)
meet(x,y,z) -> meet(x,x,y,y,z)
meet(x,y,z) -> meet(x,x,y,y,z)
meet(x,y) -> meet(x,x,y)
meet(x,y,z) -> meet(x,x,y,z,y,z)
meet(x,y) -> meet(x,y,x,y)
meet(x,y,z,w) -> meet(x,x,y,z,y,w,z,w)
meet(x,y,z) -> meet(x,y,x,z,y,z)
meet(x,y) -> meet(x,x,y,y)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y) -> meet(x,x,y,y)
meet(x,y,z,w) -> meet(x,x,y,z,z,w,y,w)
meet(x,y,z) -> meet(x,y,y,z,x,z)
meet(x,y,z,w,x1) -> meet(x,x,y,z,y,w,w,x1,z,x1)
meet(x,y,z,w) -> meet(x,y,x,z,z,w,y,w)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y,z,w) -> meet(x,x,y,y,z,z,w,w)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y,z) -> meet(x,x,y,z,y,z)
meet(x,y) -> meet(x,y,x,y)
meet(x,y,z) -> meet(x,x,y,z,z,y)
meet(x,y) -> meet(x,y,y,x)
meet(x,y,z,w) -> meet(x,x,y,z,y,w,w,z)
meet(x,y,z) -> meet(x,y,x,z,z,y)
meet(x,y,z,w) -> meet(x,x,y,z,y,z,w,w)
meet(x,y,z) -> meet(x,y,x,y,z,z)
meet(x,y,z,w,x1) -> meet(x,x,y,z,y,w,z,w,x1,x1)
meet(x,y,z,w) -> meet(x,y,x,z,y,z,w,w)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y,z,w) -> meet(x,x,y,y,z,z,w,w)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y,z,w,x1) -> meet(x,x,y,z,z,w,y,w,x1,x1)
meet(x,y,z,w) -> meet(x,y,y,z,x,z,w,w)
meet(x,y,z,w,x1,x2) -> meet(x,x,y,z,y,w,w,x1,z,x1,x2,x2)
meet(x,y,z,w,x1) -> meet(x,y,x,z,z,w,y,w,x1,x1)
meet(x,y,z,w) -> meet(x,x,y,y,z,z,w,w)
meet(x,y,z,w,x1) -> meet(x,x,y,y,z,z,w,w,x1,x1)
meet(x,y,z,w) -> meet(x,x,y,y,z,z,w,w)
meet(x,y,z,w) -> meet(x,x,y,z,y,z,w,w)
meet(x,y,z) -> meet(x,y,x,y,z,z)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y) -> meet(x,x,y,y)
meet(x,y,z,w) -> meet(x,x,y,z,z,y,w,w)
meet(x,y,z) -> meet(x,y,y,x,z,z)
meet(x,y,z,w,x1) -> meet(x,x,y,z,y,w,w,z,x1,x1)
meet(x,y,z,w) -> meet(x,y,x,z,z,y,w,w)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y,z,w) -> meet(x,x,y,y,z,z,w,w)
meet(x,y,z) -> meet(x,x,y,y,z,z)
meet(x,y,z) -> meet(x,y,y,z,z)
meet(x,y,z,w) -> meet(x,y,y,z,z,w,w)
meet(x,y,z) -> meet(x,y,y,z,z)
meet(x,y,z) -> meet(x,y,y,z,z)
meet(x,y) -> meet(x,y,y)
join(x,y) -> join(y,y,x,x)
join(x,y,z) -> join(y,z,z,x,x,y)
join(x,y) -> join(x,y,y,x)
join(x,y) -> join(y,x,x,y)
x -> join(x,x)
join(x,y,z) -> join(x,x,y,z,y,z)
join(x,y) -> join(x,y,x,y)
join(x,y,z,w) -> join(x,x,y,z,y,w,z,w)
join(x,y,z) -> join(x,y,x,z,y,z)
join(x,y) -> join(x,x,y,y)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y) -> join(x,x,y,y)
join(x,y,z,w) -> join(x,x,y,z,z,w,y,w)
join(x,y,z) -> join(x,y,y,z,x,z)
join(x,y,z,w,x1) -> join(x,x,y,z,y,w,w,x1,z,x1)
join(x,y,z,w) -> join(x,y,x,z,z,w,y,w)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y,z,w) -> join(x,x,y,y,z,z,w,w)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y,z) -> join(x,x,y,z,y,z)
join(x,y) -> join(x,y,x,y)
join(x,y,z) -> join(x,x,y,z,z,y)
join(x,y) -> join(x,y,y,x)
join(x,y,z,w) -> join(x,x,y,z,y,w,w,z)
join(x,y,z) -> join(x,y,x,z,z,y)
join(x,y,z,w) -> join(x,x,y,z,y,z,w,w)
join(x,y,z) -> join(x,y,x,y,z,z)
join(x,y,z,w,x1) -> join(x,x,y,z,y,w,z,w,x1,x1)
join(x,y,z,w) -> join(x,y,x,z,y,z,w,w)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y,z,w) -> join(x,x,y,y,z,z,w,w)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y,z,w,x1) -> join(x,x,y,z,z,w,y,w,x1,x1)
join(x,y,z,w) -> join(x,y,y,z,x,z,w,w)
join(x,y,z,w,x1,x2) -> join(x,x,y,z,y,w,w,x1,z,x1,x2,x2)
join(x,y,z,w,x1) -> join(x,y,x,z,z,w,y,w,x1,x1)
join(x,y,z,w) -> join(x,x,y,y,z,z,w,w)
join(x,y,z,w,x1) -> join(x,x,y,y,z,z,w,w,x1,x1)
join(x,y,z,w) -> join(x,x,y,y,z,z,w,w)
join(x,y,z,w) -> join(x,x,y,z,y,z,w,w)
join(x,y,z) -> join(x,y,x,y,z,z)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y) -> join(x,x,y,y)
join(x,y,z,w) -> join(x,x,y,z,z,y,w,w)
join(x,y,z) -> join(x,y,y,x,z,z)
join(x,y,z,w,x1) -> join(x,x,y,z,y,w,w,z,x1,x1)
join(x,y,z,w) -> join(x,y,x,z,z,y,w,w)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y,z,w) -> join(x,x,y,y,z,z,w,w)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y,z) -> join(x,x,y,y,z)
join(x,y,z,w) -> join(x,x,y,y,z,z,w)
join(x,y,z) -> join(x,x,y,y,z)
join(x,y,z) -> join(x,x,y,y,z)
join(x,y) -> join(x,x,y)
join(x,y,z) -> join(x,x,y,z,y,z)
join(x,y) -> join(x,y,x,y)
join(x,y,z,w) -> join(x,x,y,z,y,w,z,w)
join(x,y,z) -> join(x,y,x,z,y,z)
join(x,y) -> join(x,x,y,y)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y) -> join(x,x,y,y)
join(x,y,z,w) -> join(x,x,y,z,z,w,y,w)
join(x,y,z) -> join(x,y,y,z,x,z)
join(x,y,z,w,x1) -> join(x,x,y,z,y,w,w,x1,z,x1)
join(x,y,z,w) -> join(x,y,x,z,z,w,y,w)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y,z,w) -> join(x,x,y,y,z,z,w,w)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y,z) -> join(x,x,y,z,y,z)
join(x,y) -> join(x,y,x,y)
join(x,y,z) -> join(x,x,y,z,z,y)
join(x,y) -> join(x,y,y,x)
join(x,y,z,w) -> join(x,x,y,z,y,w,w,z)
join(x,y,z) -> join(x,y,x,z,z,y)
join(x,y,z,w) -> join(x,x,y,z,y,z,w,w)
join(x,y,z) -> join(x,y,x,y,z,z)
join(x,y,z,w,x1) -> join(x,x,y,z,y,w,z,w,x1,x1)
join(x,y,z,w) -> join(x,y,x,z,y,z,w,w)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y,z,w) -> join(x,x,y,y,z,z,w,w)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y,z,w,x1) -> join(x,x,y,z,z,w,y,w,x1,x1)
join(x,y,z,w) -> join(x,y,y,z,x,z,w,w)
join(x,y,z,w,x1,x2) -> join(x,x,y,z,y,w,w,x1,z,x1,x2,x2)
join(x,y,z,w,x1) -> join(x,y,x,z,z,w,y,w,x1,x1)
join(x,y,z,w) -> join(x,x,y,y,z,z,w,w)
join(x,y,z,w,x1) -> join(x,x,y,y,z,z,w,w,x1,x1)
join(x,y,z,w) -> join(x,x,y,y,z,z,w,w)
join(x,y,z,w) -> join(x,x,y,z,y,z,w,w)
join(x,y,z) -> join(x,y,x,y,z,z)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y) -> join(x,x,y,y)
join(x,y,z,w) -> join(x,x,y,z,z,y,w,w)
join(x,y,z) -> join(x,y,y,x,z,z)
join(x,y,z,w,x1) -> join(x,x,y,z,y,w,w,z,x1,x1)
join(x,y,z,w) -> join(x,y,x,z,z,y,w,w)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y,z,w) -> join(x,x,y,y,z,z,w,w)
join(x,y,z) -> join(x,x,y,y,z,z)
join(x,y,z) -> join(x,y,y,z,z)
join(x,y,z,w) -> join(x,y,y,z,z,w,w)
join(x,y,z) -> join(x,y,y,z,z)
join(x,y,z) -> join(x,y,y,z,z)
join(x,y) -> join(x,y,y)