Variations on the topic of the USE Informatics forum "Another proof of Helen Mironchick's paradigm" - Solving one system of equations in Boolean variables in the style of 08.2016 "GRAPHES AND SYSTEMS OF LOGICAL EQUATIONS"

The source system is described by the digrams in the style of 08.2016 and immediately calculated

  ((x1≡x2)≡x3)=>((x4=>x5)=>x6)=1
  ((x4≡x5)≡x6)=>((x7=>x8)=>x9)=1
  ((x7≡x8)≡x9)=>((x1=>x2)=>x3)=1
System calculation
  ((x1≡x2)≡x3)=>((x4=>x5)=>x6)=1
  ((x4≡x5)≡x6)=>((x7=>x8)=>x9)=1
in first table 
System calculation
  ((x1≡x2)≡x3)=>((x4=>x5)=>x6)=1
  ((x4≡x5)≡x6)=>((x7=>x8)=>x9)=1
  ((x7≡x8)≡x9)=>((x1=>x2)=>x3)=0
in second table

 In the second table, we start the run by setting "2' and "1" values for 3-bit groups, where  (x1=> x2) =>x3 = 0. Upon completion, we count the number (x7≡x8) ≡ x9 equal to 1  in the last column, where, generally speaking, there are bit triples associated with  (x7=>x8) =>x9. 
In the green group (3 triples 001,100,111) and (x7=>x8)=>x9 = (x7≡x8 )≡x9 equal to 1
In the gray group (1 triple 010) and (x7=>x8)=>x9 = 0 ,
but (x7≡x8)≡x9 = 1 

  Passing Polyakov's Control