Monday, September 17, 2018

Метод Отображений vs Метод битовых масок (once again). Нетривиальные возможности метода отображений (Графы и системы булевых уравнений по Е. А. Мирончик 08/2016 )


    For version in English just view the previous post to same blog

  Систему немного сложнее решить в сравнении с P-34 (в скобках содержатся только xj, yj, zj) , другими словами, с 3-значными ключами.      
P-34 может быть решена через пару минут, просто просматривая таблицу битовой маски {X}  и вычисляя сумму решений для каждой строки {X}.
  Четыре переменные в скобках приводят к проблеме в использовании метода битовых масок для генерации простых (y, z) систем для каждой строки из {X}. Таким образом, это наглядно демонстрирует преимущество
метода статьи "Графы и Системы логических уравнений"  Елены Мирончик (08/2016)

(x1=>x2)^(x2=>x3)^(x3=>x4)^(x4=>x5)=1
(¬x1+y1+z1+w1)^(x1+¬y1+z1+w1)^(x1+y1+¬z1+w1)^(x1+y1+z1+¬w1)=1
(¬x2+y2+z2+w2)^(x2+¬y2+z2+w2)^(x2+y2+¬z2+w2)^(x2+y2+z2+¬w2)=1 
(¬x3+y3+z3+w3)^(x3+¬y3+z3+w3)^(x3+y3+¬z3+w3)^(x3+y3+z3+¬w3)=1
(¬x4+y4+z4+w4)^(x4+¬y4+z4+w4)^(x4+y4+¬z4+w4)^(x4+y4+z4+¬w4)=1
(¬x5+y5+z5+w4)^(x5+¬y5+z5+w4)^(x5+y5+¬z5+w4)^(x5+y5+z5+¬w5)=1

           Конвертируем систему



(x1=>x2)^(¬x1+y1+z1+w1)^(x1+¬y1+z1+w1)^(x1+y1+¬z1+w1)^(x1+y1+z1+¬w1)=1
(x2=>x3)^(¬x2+y2+z2+w2)^(x2+¬y2+z2+w2)^(x2+y2+¬z2+w2)^(x2+y2+z2+¬w2)=1  
(x3=>x4)^(¬x3+y3+z3+w3)^(x3+¬y3+z3+w3)^(x3+y3+¬z3+w3)^(x3+y3+z3+¬w3)=1
(x4=>x5)^(¬x4+y4+z4+w4)^(x4+¬y4+z4+w4)^(x4+y4+¬z4+w4)^(x4+y4+z4+¬w4)=1
      (¬x5+y5+z5+w5)^(x5+¬y5+z5+w5)^(x5+y5+¬z5+w5)^(x5+y5+z5+¬w5)=1

Мы собираемся построить первую часть графа. Следующие четыре части за первой должны быть точно такими же, как и первая . Мы можем добавить три цифры (чтобы построить ключ). Корректный  способ получения четырехзначного ключа не позволяет ему иметь только одну цифру «1». Потому,что это приведет к тому, что одна из скобок (логических множителей) будет равна «0». Эта скобка будет иметь «¬» в позиции, где ключ имеет «1»,  а все остальные переменные соответственно маске ключа  будут равны «0» 
   

                                              Весь граф


Контроль по Полякову



     Рассмотрим еще один пример
    

Конвертируем систему

(x1=>x2)^(x2=>x3)^(x3=>x4)^(x4=>x5)=1
((¬x1^y1^z1^w1) v (x1^¬y1^z1^w1) v (x1^y1^¬z1^w1) v (x1^y1^z1^¬w1)) =1
((¬x2^y2^z2^w2) v (x2^¬y2^z2^w2) v (x2^y2^¬z2^w2) v (x2^y2^z2^¬w2)) =1
((¬x3^y3^z3^w3) v (x3^¬y3^z3^w3) v (x3^y3^¬z3^w3) v (x3^y3^z3^¬w3)) =1
((¬x4^y4^z4^w4) v (x4^¬y4^z4^w4) v (x4^y4^¬z4^w4) v (x4^y4^z4^¬w4)) =1
((¬x5^y5^z5^w5) v (x5^¬y5^z5^w5) v (x5^y5^¬z5^w5) v (x5^y5^z5^¬w5)) =1
   
к виду

(x1=>x2)^((¬x1^y1^z1^w1) v (x1^¬y1^z1^w1) v (x1^y1^¬z1^w1) v (x1^y1^z1^¬w1)) =1
(x2=>x3)^((¬x2^y2^z2^w2) v (x2^¬y2^z2^w2) v (x2^y2^¬z2^w2) v (x2^y2^z2^¬w2)) =1
(x3=>x4)^((¬x3^y3^z3^w3) v (x3^¬y3^z3^w3) v (x3^y3^¬z3^w3) v (x3^y3^z3^¬w3)) =1
(x4=>x5)^((¬x4^y4^z4^w4) v (x4^¬y4^z4^w4) v (x4^y4^¬z4^w4) v (x4^y4^z4^¬w4)) =1
((¬x5^y5^z5^w5) v (x5^¬y5^z5^w5) v (x5^y5^¬z5^w5) v (x5^y5^z5^¬w5)) =1

Построим полный граф


   Контроль по Полякову


Wednesday, September 5, 2018

Unleash the full power of the Mapping Method (Graphs and Systems of Boolean Equations by E.A. Mironchik) (P-34 with xj,yj,zj,wj ; j=1,.,5 for five conditional equations)

Consider following system


System is a bit harder to treat vs P-34 itself (brackets contain only xj,yj,zj )
in other words 3 digits keys configuration. Why I believe it's worth to analyze ?
P-34 may be solved in a couple of minutes just scanning through {X} bitmask table and calculating sum of solutions  for each row of {X}.
Four variables in brackets result  bitmask approach failure to generate
simple (y,z) systems for each row in {X}. Thus it clearly demonstrates
an advantage of "Graph&&Mapping method"  idea by Helen Mironchick

(x1=>x2)^(x2=>x3)^(x3=>x4)^(x4=>x5)=1
(¬x1+y1+z1+w1)^(x1+¬y1+z1+w1)^(x1+y1+¬z1+w1)^(x1+y1+z1+¬w1)=1
(¬x2+y2+z2+w2)^(x2+¬y2+z2+w2)^(x2+y2+¬z2+w2)^(x2+y2+z2+
¬w2)=1  
(¬x3+y3+z3+w3)^(x3+¬y3+z3+w3)^(x3+y3+¬z3+w3)^(x3+y3+z3+¬w3)=1
(¬x4+y4+z4+w4)^(x4+¬y4+z4+w4)^(x4+y4+¬z4+w4)^(x4+y4+z4+¬w4)=1
(¬x5+y5+z5+w4)^(x5+¬y5+z5+w4)^(x5+y5+¬z5+w4)^(x5+y5+z5+¬w5)=1

            Convert system as follows

(x1=>x2)^(¬x1+y1+z1+w1)^(x1+¬y1+z1+w1)^(x1+y1+¬z1+w1)^(x1+y1+z1+¬w1)=1
(x2=>x3)^(¬x2+y2+z2+w2)^(x2+¬y2+z2+w2)^(x2+y2+¬z2+w2)^(x2+y2+z2+¬w2)=1  
(x3=>x4)^(¬x3+y3+z3+w3)^(x3+¬y3+z3+w3)^(x3+y3+¬z3+w3)^(x3+y3+z3+¬w3)=1
(x4=>x5)^(¬x4+y4+z4+w4)^(x4+¬y4+z4+w4)^(x4+y4+¬z4+w4)^(x4+y4+z4+¬w4)=1
      (¬x5+y5+z5+w5)^(x5+¬y5+z5+w5)^(x5+y5+¬z5+w5)^(x5+y5+z5+¬w5)=1

We are going to build the first  share of the graph .
The next four shares following first one are supposed to be exactly the same as first.
We may add three digits  (to build key). The only way resulting four digits key doesn't allow it to have the only one digit "1". Because it would result  one of brackets (logical
multipliers) to be "0" .  Those bracket would  have "¬"  on position where key has "1" and all other  digits equal "0"


See http://kpolyakov.spb.ru/download/mea-2016-8.pdf   for core ideas and file
ege23.doc on Polyakov's site kpolyakov.spb.ru/download/ege23.doc  
P-34 sample ( it uses three digits keys vs four digits in our case )
 

                                   
                                        Complete graph diagram
 

     Pass Polyakov's control   


 
 

  


 

Monday, September 3, 2018

Unleash the full power of the Mapping Method (Graphs and Systems of Boolean Equations by E.A. Mironchik)

Consider foillowing system

Why I believe it's worth to analyze ? Original task ( just xj,yj,zj in every bracket)  may be solved in a couple of minutes just scanning through {X} bitmask table and calculating sum of solutions  for each row of {X}. Four variables in brackets result  bitmask approach failure to generate simple (y,z) systems for each row in {X}. Thus it clearly demonstrates an advantage of "Graph&&Mapping method"  idea by Helen Mironchick

(x1=>x2)^(x2=>x3)^(x3=>x4)^(x4=>x5)=1
((¬x1^y1^z1^w1) v (x1^¬y1^z1^w1) v (x1^y1^¬z1^w1) v (x1^y1^z1^¬w1)) =1
((¬x2^y2^z2^w2) v (x2^¬y2^z2^w2) v (x2^y2^¬z2^w2) v (x2^y2^z2^¬w2)) =1
((¬x3^y3^z3^w3) v (x3^¬y3^z3^w3) v (x3^y3^¬z3^w3) v (x3^y3^z3^¬w3)) =1
((¬x4^y4^z4^w4) v (x4^¬y4^z4^w4) v (x4^y4^¬z4^w4) v (x4^y4^z4^¬w4)) =1
((¬x5^y5^z5^w5) v (x5^¬y5^z5^w5) v (x5^y5^¬z5^w5) v (x5^y5^z5^¬w5)) =1

Convert system as follows

(x1=>x2)^((¬x1^y1^z1^w1) v (x1^¬y1^z1^w1) v (x1^y1^¬z1^w1) v (x1^y1^z1^¬w1)) =1
(x2=>x3)^((¬x2^y2^z2^w2) v (x2^¬y2^z2^w2) v (x2^y2^¬z2^w2) v (x2^y2^z2^¬w2)) =1
(x3=>x4)^((¬x3^y3^z3^w3) v (x3^¬y3^z3^w3) v (x3^y3^¬z3^w3) v (x3^y3^z3^¬w3)) =1
(x4=>x5)^((¬x4^y4^z4^w4) v (x4^¬y4^z4^w4) v (x4^y4^¬z4^w4) v (x4^y4^z4^¬w4)) =1
((¬x5^y5^z5^w5) v (x5^¬y5^z5^w5) v (x5^y5^¬z5^w5) v (x5^y5^z5^¬w5)) =1

Build complete graph for system

    Pass system via Polyakov's Control

References

Saturday, September 1, 2018

The method of mappings (graphs and systems of logical equations) vs The method of bit masks by the example of one known system from the VKontakte newswire with a dimension of 10 instead of 4


The system is traditionally solved by the method of bitmask masks,
since for X-th this is a well-known upper triangular matrix and it
remains to calculate the number of solutions for each of its rows,
which is not very difficult for 4 implications, but for 9 implications
with a corresponding matrix of 10 rows it will already become somewhat
tedious (manually).

Bellow follows the solution based on the construction of a complete graph
of the system with the subsequent application of the technique proposed
by E.A. Mironchik [ 1 ]. Consider a system where the use of bit masks will
require a large number of calculations and convert it as follows
 
Convert the system  :-

(x1=>x2)^(x2=>x3)^(x3=>x4)^(x4=>x5)^(x5=>x6)^(x6=>x7)^
^(x7=>x8)^(x8=>x9)^(x9=>x10)=1
((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1
((¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4)) =1
((¬x5^y5^z5) v (x5^¬y5^z5) v (x4^y5^¬z5)) =1
((¬x6^y6^z6) v (x6^¬y6^z6) v (x6^y6^¬z6)) =1
((¬x7^y7^z7) v (x6^¬y6^z7) v (x7^y7^¬z7)) =1
((¬x8^y8^z8) v (x8^¬y8^z8) v (x8^y8^¬z8)) =1
((¬x9^y9^z9) v (x9^¬y9^z9) v (x9^y9^¬z9)) =1
((¬x10^y10^z10) v (x10^¬y10^z10) v (x10^y10^¬z10)) =1


Build a complete graph for system bellow :-

  (x1=>x2)^((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
  (x2=>x3)^((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
  (x3=>x4)^((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1  
  (x4=>x5)^((¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4)) =1
  (x5=>x6)^((¬x5^y5^z5) v (x5^¬y5^z5) v (x4^y5^¬z5)) =1
  (x6=>x7)^((¬x6^y6^z6) v (x6^¬y6^z6) v (x6^y6^¬z6)) =1
  (x7=>x8)^((¬x7^y7^z7) v (x6^¬y6^z7) v (x7^y7^¬z7)) =1
  (x8=>x9)^((¬x8^y8^z8) v (x8^¬y8^z8) v (x8^y8^¬z8)) =1
  (x9=>x10)^((¬x9^y9^z9) v (x9^¬y9^z9) v (x9^y9^¬z9)) =1
  ((¬x10^y10^z10) v (x10^¬y10^z10) v (x10^y10^¬z10)) =1



Wednesday, August 29, 2018

Решение Методом Отображений клона одного из примеров оригинальной работы Е.А.Мирончик "Информатика в школе" 10/2013

Модифицируем пример из http://kpolyakov.spb.ru/download/mea-2013-10.pdf



Сделаем  замену  "*"  на "+"

((((( x1 v x2 ) =>x3 ) v x4 ) =>x5 ) v x6 ) => x7 = 1 (1)

В старой нотации

(((( (x1+x2 )->x3 ) +x4 ) ->x5 ) + x6 -> x7 = 1  (2)

Воспроизведем  логику оригинального примера на (1)



  Контроль (2) по Полякову



Saturday, August 25, 2018

Метод Отображений (графы и системы логических уравнений) vs Метод битовых масок .Решение одной системы логических уравнений по Е.А.Мирончик (mea-2016-8.pdf)


(x1vx2)^(x2vx3)^(x3vx4)^(x4vx5)=1
((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1
((¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4)) =1
((¬x5^y5^z5) v (x5^¬y5^z5) v (x5^y5^¬z5)) =1

Конвертируем систему

(x1vx2)^((!x1^y1^z1) v (x1^!y1^z1) v (x1^y1^!z1)) =1
(x2vx3)^((!x2^y2^z2) v (x2^!y2^z2) v (x2^y2^!z2)) =1
(x3vx4)^((!x3^y3^z3) v (x3^!y3^z3) v (x3^y3^!z3)) =1
(x4vx5)^((!x4^y4^z4) v (x4^!y4^z4) v (x4^y4^!z4)) =1
((!x5^y5^z5) v (x5^!y5^z5) v (x5^y5^!z5)) =1

Строим полный граф системы, следуя
http://kpolyakov.spb.ru/download/mea-2016-8.pdf


   Контроль на сервере Полякова


     Рассмотрим еще один пример эффективности метода


 
Конвертируем систему :-

(x1=>x2)^(x2=>x3)^(x3=>x4)^(x4=>x5)^(x5=>x6)^(x6=>x7)^
^(x7=>x8)^(x8=>x9)^(x9=>x10)=1
((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1
((¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4)) =1
((¬x5^y5^z5) v (x5^¬y5^z5) v (x4^y5^¬z5)) =1
((¬x6^y6^z6) v (x6^¬y6^z6) v (x6^y6^¬z6)) =1
((¬x7^y7^z7) v (x6^¬y6^z7) v (x7^y7^¬z7)) =1
((¬x8^y8^z8) v (x8^¬y8^z8) v (x8^y8^¬z8)) =1
((¬x9^y9^z9) v (x9^¬y9^z9) v (x9^y9^¬z9)) =1
((¬x10^y10^z10) v (x10^¬y10^z10) v (x10^y10^¬z10)) =1


   Строим полный граф системы

  (x1=>x2)^((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
  (x2=>x3)^((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
  (x3=>x4)^((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1  
  (x4=>x5)^((¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4)) =1
  (x5=>x6)^((¬x5^y5^z5) v (x5^¬y5^z5) v (x4^y5^¬z5)) =1
  (x6=>x7)^((¬x6^y6^z6) v (x6^¬y6^z6) v (x6^y6^¬z6)) =1
  (x7=>x8)^((¬x7^y7^z7) v (x6^¬y6^z7) v (x7^y7^¬z7)) =1
  (x8=>x9)^((¬x8^y8^z8) v (x8^¬y8^z8) v (x8^y8^¬z8)) =1
  (x9=>x10)^((¬x9^y9^z9) v (x9^¬y9^z9) v (x9^y9^¬z9)) =1
  ((¬x10^y10^z10) v (x10^¬y10^z10) v (x10^y10^¬z10)) =1


Friday, August 17, 2018

Метод Отображений (графы и системы логических уравнений) vs Метод битовых масок на примере одной известной системы из новостной ленты ВК


   Система традиционно решается методом битовых масок, так как для Х-ов это хорошо известная верхнетреугольная матрица и остается подсчитать число решений для каждой из ее строк , что не представляет особой трудности.

   Ниже следует решение основанное на построении полного графа системы с последующим примением техники предложенной Е.А.Мирончик [ 1 ]  . Построение полного графа для данной системы[
(x1->x2)^(x2->x3)^(x3->x4) =1
(¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1) =1
(¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2) =1
(¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3) =1
(¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4) =1

Конвертируем систему следующим образом

(x1=>x2)^((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
(x2=>x3)^((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
(x3=>x4)^((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1
(¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4) =1
 
Когда х1=0 есть лишь одна пара y=1 ; z1=1
иначе есть две пары
y1=0 ; z1 =1
y1=1 ; z1=0



  Стандартное решение чез битовую маску для {х}
  дает тот же результат 31



Рассмотрим систему, где  использование битовых масок потребует большего количества вычислений и конвертируем ее следующим образом

(x1=>x2)^(x2=>x3)^(x3=>x4)(x4=>x5)^(x5=>x6)^(x6=>x7)=1
((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1
((¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4)) =1
((¬x5^y5^z5) v (x5^¬y5^z5) v (x4^y5^¬z5)) =1
((¬x6^y6^z6) v (x6^¬y6^z6) v (x6^y6^¬z6)) =1
((¬x7^y7^z7) v (x7^¬y7^z7) v (x7^y7^¬z7)) =1

Конвертированная система

(x1=>x2)^((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
(x2=>x3)^((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
(x3=>x4)^((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1
(x4=>x5)^((¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4)) =1
(x5=>x6)^((¬x5^y5^z5) v (x5^¬y5^z5) v (x4^y5^¬z5)) =1
(x6=>x7)^((¬x6^y6^z6) v (x6^¬y6^z6) v (x6^y6^¬z6)) =1
((¬x7^y7^z7) v (x7^¬y7^z7) v (x7^y7^¬z7)) =1

Строим полный граф для последней системы.В отличие от битовых масок увеличение размеров матрицы обрабатывется без длинных вычислений.
Поведение графа системы при ее увеличение числа
импликации, например до 7:-


 Тестируем ответ на Сервере Полякова


   Другой пример. В этом случае битовая маска для Х  отнюдь не очевидна
       

  
       (x1+x2)^(x2+x3)^(x3+x4)=1
       ((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
       ((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
       ((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1
       ((¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4)) =1

   Конвертируем систему

       (x1+x2)*((!x1*y1*z1) + (x1*!y1*z1) + (x1*y1*!z1)) =1
       (x2+x3)*((!x2*y2*z2) + (x2*!y2*z2) + (x2*y2*!z2)) =1
       (x3+x4)*((!x3*y3*z3) + (x3*!y3*z3) + (x3*y3*!z3)) =1
       ((!x4*y4*z4) + (x4*!y4*z4) + (x4*y4*!z4)) =1



   Контроль

   

Сравним  с образцом Р-34 из ege23.doc. Думаю,что текст конвертированной системы Р-34 содержит опечатку либо случайную неточность.



   Думаю, что правильная  версия системы в образце - следующая
  
  Протестируем уравнение Р-34, конвертированное несколько иначе
   чем на первом снапшоте вверху :-

   (x1=>x2)^(¬x1vy1vz1)^(x1v¬y1vz1)^(x1vy1v¬z1)=1
   (x2=>x3)^(¬x2vy2vz2)^(x2v¬y2vz2)^(x2vy2v¬z2)=1
   (x3=>x4)^(¬x3vy3vz3)^(x3v¬y3vz3)^(x3vy3v¬z3)=1
         (¬x4vy4vz4)^(x4v¬y4vz4)^(x4vy4v¬z4)=1

  
   Результат сервера подтверждает, что поданная на вход система корректна.Рассмотрим систему №150 из ege23.doc
  

    Конвертируем ее следующим образом ( отличным от Р-34 )

     (x1=>x2)^(¬x1vy1vz1)^(x1v¬y1vz1)^(x1vy1v¬z1)=1
     (x2=>x3)^(¬x2vy2vz2)^(x2v¬y2vz2)^(x2vy2v¬z2)=1      
     (x3=>x4)^(¬x3vy3vz3)^(x3v¬y3vz3)^(x3vy3v¬z3)=1
     (x4=>x5)^(¬x4vy4vz4)^(x4v¬y4vz4)^(x4vy4v¬z4)=1
            (¬x5vy5vz5)^(x5v¬y5vz5)^(x5vy5v¬z5)=1

    Построим диаграмму следуя Е.А. Мирончик
   

   Проверим систему на сервере Полякова
  

   
    Литература
    1. http://kpolyakov.spb.ru/download/mea-2016-8.pdf