This work by Gennady Davydov and Inna Davydova was presented at 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods (Tableaux96) held in Terrasini (Palermo, Italy) during May 15-17, 1996.