Z3---4.15.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : Z3---4.15.1
% Problem  : SWV227+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% Transfm  : none
% Format   : tptp
% Command  : run_E %s %d THM

% Computer : n010.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Sat Jun 21 05:31:47 AM UTC 2025

% Result   : Theorem 0.20s 0.38s
% Output   : Proof 0.20s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   11
%            Number of leaves      :   16
% Syntax   : Number of formulae    :   39 (   2 unt;   0 typ;   0 def)
%            Number of atoms       : 5583 (5271 equ)
%            Maximal formula atoms :  102 ( 143 avg)
%            Number of connectives : 7809 (2418   ~; 238   |;4997   &)
%                                         ( 113 <=>;  43  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   32 (  13 avg)
%            Maximal term depth    :    2 (   1 avg)
%            Number of FOOLs       :  153 ( 153 fml;   0 var)
%            Number of types       :    2 (   0 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :    8 (   5 usr;   2 prp; 0-3 aty)
%            Number of functors    :   11 (  11 usr;   9 con; 0-3 aty)
%            Number of variables   :   64 (  62   !;   0   ?;  64   :)

% Comments : 
%------------------------------------------------------------------------------
tff(n0_type,type,
    n0: $i ).

tff(a_select2_type,type,
    a_select2: ( $i * $i ) > $i ).

tff(n4_type,type,
    n4: $i ).

tff(xinit_noise_type,type,
    xinit_noise: $i ).

tff(n5_type,type,
    n5: $i ).

tff(n2_type,type,
    n2: $i ).

tff(n3_type,type,
    n3: $i ).

tff(n1_type,type,
    n1: $i ).

tff(leq_type,type,
    leq: ( $i * $i ) > $o ).

tff(a_select3_type,type,
    a_select3: ( $i * $i * $i ) > $i ).

tff(r_ds1_filter_type,type,
    r_ds1_filter: $i ).

tff(q_ds1_filter_type,type,
    q_ds1_filter: $i ).

tff(1,plain,
    ( ~ $true
  <=> $false ),
    inference(rewrite,[status(thm)],[]) ).

tff(2,plain,
    ( ( ( ! [A: $i,B: $i] :
            ( ~ ( leq(n0,A)
                & leq(n0,B)
                & leq(A,n5)
                & leq(B,n5) )
            | ( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ) )
        & ! [C: $i,D: $i] :
            ( ~ ( leq(n0,C)
                & leq(n0,D)
                & leq(C,n2)
                & leq(D,n2) )
            | ( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ) ) )
     => $true )
  <=> $true ),
    inference(rewrite,[status(thm)],[]) ).

tff(3,plain,
    ( ( ( a_select2(xinit_noise,n4) = n0 )
      | ~ leq(n2,n5)
      | ( ( n0 = n5 )
        & ( n3 = n2 ) )
      | ( ( n0 = n5 )
        & ( n4 = n2 ) )
      | ( ( n0 = n5 )
        & ( n5 = n2 ) )
      | ( n0 = n2 )
      | ( ( n1 = n5 )
        & ( n3 = n2 ) )
      | ( ( n1 = n5 )
        & ( n4 = n2 ) )
      | ( ( n1 = n5 )
        & ( n5 = n2 ) )
      | ( n1 = n2 )
      | ( ( n2 = n5 )
        & ( n3 = n2 ) )
      | ( ( n2 = n5 )
        & ( n4 = n2 ) )
      | ( ( n2 = n5 )
        & ( n5 = n2 ) )
      | $true
      | ( ( n3 = n5 )
        & ( n3 = n2 ) )
      | ( ( n3 = n5 )
        & ( n4 = n2 ) )
      | ( ( n3 = n5 )
        & ( n5 = n2 ) )
      | ( ( n3 = n2 )
        & ( n4 = n5 ) )
      | ( n3 = n2 )
      | ( ( n4 = n5 )
        & ( n4 = n2 ) )
      | ( ( n4 = n5 )
        & ( n5 = n2 ) )
      | ( n4 = n2 )
      | ( n5 = n2 )
      | ( n4 != n5 )
      | ( n4 != n2 )
      | ~ leq(n0,n5)
      | ~ leq(n0,n2)
      | ~ leq(n5,n5) )
  <=> $true ),
    inference(rewrite,[status(thm)],[]) ).

tff(4,plain,
    ( ( $true
      & ( n5 = n2 ) )
  <=> ( n5 = n2 ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(5,plain,
    ( ( n5 = n5 )
  <=> $true ),
    inference(rewrite,[status(thm)],[]) ).

tff(6,plain,
    ( ( ( n5 = n5 )
      & ( n5 = n2 ) )
  <=> ( $true
      & ( n5 = n2 ) ) ),
    inference(monotonicity,[status(thm)],[5]) ).

tff(7,plain,
    ( ( ( n5 = n5 )
      & ( n5 = n2 ) )
  <=> ( n5 = n2 ) ),
    inference(transitivity,[status(thm)],[6,4]) ).

tff(8,plain,
    ( ( ( n4 = n2 )
      & $true )
  <=> ( n4 = n2 ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(9,plain,
    ( ( ( n4 = n2 )
      & ( n5 = n5 ) )
  <=> ( ( n4 = n2 )
      & $true ) ),
    inference(monotonicity,[status(thm)],[5]) ).

tff(10,plain,
    ( ( ( n4 = n2 )
      & ( n5 = n5 ) )
  <=> ( n4 = n2 ) ),
    inference(transitivity,[status(thm)],[9,8]) ).

tff(11,plain,
    ( ( ( n3 = n2 )
      & $true )
  <=> ( n3 = n2 ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(12,plain,
    ( ( ( n3 = n2 )
      & ( n5 = n5 ) )
  <=> ( ( n3 = n2 )
      & $true ) ),
    inference(monotonicity,[status(thm)],[5]) ).

tff(13,plain,
    ( ( ( n3 = n2 )
      & ( n5 = n5 ) )
  <=> ( n3 = n2 ) ),
    inference(transitivity,[status(thm)],[12,11]) ).

tff(14,plain,
    ( ( $true
      & $true )
  <=> $true ),
    inference(rewrite,[status(thm)],[]) ).

tff(15,plain,
    ( ( n2 = n2 )
  <=> $true ),
    inference(rewrite,[status(thm)],[]) ).

tff(16,plain,
    ( ( ( n2 = n2 )
      & ( n5 = n5 ) )
  <=> ( $true
      & $true ) ),
    inference(monotonicity,[status(thm)],[15,5]) ).

tff(17,plain,
    ( ( ( n2 = n2 )
      & ( n5 = n5 ) )
  <=> $true ),
    inference(transitivity,[status(thm)],[16,14]) ).

tff(18,plain,
    ( ( ( n1 = n2 )
      & $true )
  <=> ( n1 = n2 ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(19,plain,
    ( ( ( n1 = n2 )
      & ( n5 = n5 ) )
  <=> ( ( n1 = n2 )
      & $true ) ),
    inference(monotonicity,[status(thm)],[5]) ).

tff(20,plain,
    ( ( ( n1 = n2 )
      & ( n5 = n5 ) )
  <=> ( n1 = n2 ) ),
    inference(transitivity,[status(thm)],[19,18]) ).

tff(21,plain,
    ( ( ( n0 = n2 )
      & $true )
  <=> ( n0 = n2 ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(22,plain,
    ( ( ( n0 = n2 )
      & ( n5 = n5 ) )
  <=> ( ( n0 = n2 )
      & $true ) ),
    inference(monotonicity,[status(thm)],[5]) ).

tff(23,plain,
    ( ( ( n0 = n2 )
      & ( n5 = n5 ) )
  <=> ( n0 = n2 ) ),
    inference(transitivity,[status(thm)],[22,21]) ).

tff(24,plain,
    ( ( ( a_select2(xinit_noise,n4) = n0 )
      | ~ leq(n2,n5)
      | ( ( n0 = n5 )
        & ( n3 = n2 ) )
      | ( ( n0 = n5 )
        & ( n4 = n2 ) )
      | ( ( n0 = n5 )
        & ( n5 = n2 ) )
      | ( ( n0 = n2 )
        & ( n5 = n5 ) )
      | ( ( n1 = n5 )
        & ( n3 = n2 ) )
      | ( ( n1 = n5 )
        & ( n4 = n2 ) )
      | ( ( n1 = n5 )
        & ( n5 = n2 ) )
      | ( ( n1 = n2 )
        & ( n5 = n5 ) )
      | ( ( n2 = n5 )
        & ( n3 = n2 ) )
      | ( ( n2 = n5 )
        & ( n4 = n2 ) )
      | ( ( n2 = n5 )
        & ( n5 = n2 ) )
      | ( ( n2 = n2 )
        & ( n5 = n5 ) )
      | ( ( n3 = n5 )
        & ( n3 = n2 ) )
      | ( ( n3 = n5 )
        & ( n4 = n2 ) )
      | ( ( n3 = n5 )
        & ( n5 = n2 ) )
      | ( ( n3 = n2 )
        & ( n4 = n5 ) )
      | ( ( n3 = n2 )
        & ( n5 = n5 ) )
      | ( ( n4 = n5 )
        & ( n4 = n2 ) )
      | ( ( n4 = n5 )
        & ( n5 = n2 ) )
      | ( ( n4 = n2 )
        & ( n5 = n5 ) )
      | ( ( n5 = n5 )
        & ( n5 = n2 ) )
      | ( n4 != n5 )
      | ( n4 != n2 )
      | ~ leq(n0,n5)
      | ~ leq(n0,n2)
      | ~ leq(n5,n5) )
  <=> ( ( a_select2(xinit_noise,n4) = n0 )
      | ~ leq(n2,n5)
      | ( ( n0 = n5 )
        & ( n3 = n2 ) )
      | ( ( n0 = n5 )
        & ( n4 = n2 ) )
      | ( ( n0 = n5 )
        & ( n5 = n2 ) )
      | ( n0 = n2 )
      | ( ( n1 = n5 )
        & ( n3 = n2 ) )
      | ( ( n1 = n5 )
        & ( n4 = n2 ) )
      | ( ( n1 = n5 )
        & ( n5 = n2 ) )
      | ( n1 = n2 )
      | ( ( n2 = n5 )
        & ( n3 = n2 ) )
      | ( ( n2 = n5 )
        & ( n4 = n2 ) )
      | ( ( n2 = n5 )
        & ( n5 = n2 ) )
      | $true
      | ( ( n3 = n5 )
        & ( n3 = n2 ) )
      | ( ( n3 = n5 )
        & ( n4 = n2 ) )
      | ( ( n3 = n5 )
        & ( n5 = n2 ) )
      | ( ( n3 = n2 )
        & ( n4 = n5 ) )
      | ( n3 = n2 )
      | ( ( n4 = n5 )
        & ( n4 = n2 ) )
      | ( ( n4 = n5 )
        & ( n5 = n2 ) )
      | ( n4 = n2 )
      | ( n5 = n2 )
      | ( n4 != n5 )
      | ( n4 != n2 )
      | ~ leq(n0,n5)
      | ~ leq(n0,n2)
      | ~ leq(n5,n5) ) ),
    inference(monotonicity,[status(thm)],[23,20,17,13,10,7]) ).

tff(25,plain,
    ( ( ( a_select2(xinit_noise,n4) = n0 )
      | ~ leq(n2,n5)
      | ( ( n0 = n5 )
        & ( n3 = n2 ) )
      | ( ( n0 = n5 )
        & ( n4 = n2 ) )
      | ( ( n0 = n5 )
        & ( n5 = n2 ) )
      | ( ( n0 = n2 )
        & ( n5 = n5 ) )
      | ( ( n1 = n5 )
        & ( n3 = n2 ) )
      | ( ( n1 = n5 )
        & ( n4 = n2 ) )
      | ( ( n1 = n5 )
        & ( n5 = n2 ) )
      | ( ( n1 = n2 )
        & ( n5 = n5 ) )
      | ( ( n2 = n5 )
        & ( n3 = n2 ) )
      | ( ( n2 = n5 )
        & ( n4 = n2 ) )
      | ( ( n2 = n5 )
        & ( n5 = n2 ) )
      | ( ( n2 = n2 )
        & ( n5 = n5 ) )
      | ( ( n3 = n5 )
        & ( n3 = n2 ) )
      | ( ( n3 = n5 )
        & ( n4 = n2 ) )
      | ( ( n3 = n5 )
        & ( n5 = n2 ) )
      | ( ( n3 = n2 )
        & ( n4 = n5 ) )
      | ( ( n3 = n2 )
        & ( n5 = n5 ) )
      | ( ( n4 = n5 )
        & ( n4 = n2 ) )
      | ( ( n4 = n5 )
        & ( n5 = n2 ) )
      | ( ( n4 = n2 )
        & ( n5 = n5 ) )
      | ( ( n5 = n5 )
        & ( n5 = n2 ) )
      | ( n4 != n5 )
      | ( n4 != n2 )
      | ~ leq(n0,n5)
      | ~ leq(n0,n2)
      | ~ leq(n5,n5) )
  <=> $true ),
    inference(transitivity,[status(thm)],[24,3]) ).

tff(26,plain,
    ( ! [E: $i,F: $i] :
        ( ( a_select2(xinit_noise,n4) = n0 )
        | ~ leq(n2,n5)
        | ( ( n0 = n5 )
          & ( n3 = n2 ) )
        | ( ( n0 = n5 )
          & ( n4 = n2 ) )
        | ( ( n0 = n5 )
          & ( n5 = n2 ) )
        | ( ( n0 = n2 )
          & ( n5 = n5 ) )
        | ( ( n1 = n5 )
          & ( n3 = n2 ) )
        | ( ( n1 = n5 )
          & ( n4 = n2 ) )
        | ( ( n1 = n5 )
          & ( n5 = n2 ) )
        | ( ( n1 = n2 )
          & ( n5 = n5 ) )
        | ( ( n2 = n5 )
          & ( n3 = n2 ) )
        | ( ( n2 = n5 )
          & ( n4 = n2 ) )
        | ( ( n2 = n5 )
          & ( n5 = n2 ) )
        | ( ( n2 = n2 )
          & ( n5 = n5 ) )
        | ( ( n3 = n5 )
          & ( n3 = n2 ) )
        | ( ( n3 = n5 )
          & ( n4 = n2 ) )
        | ( ( n3 = n5 )
          & ( n5 = n2 ) )
        | ( ( n3 = n2 )
          & ( n4 = n5 ) )
        | ( ( n3 = n2 )
          & ( n5 = n5 ) )
        | ( ( n4 = n5 )
          & ( n4 = n2 ) )
        | ( ( n4 = n5 )
          & ( n5 = n2 ) )
        | ( ( n4 = n2 )
          & ( n5 = n5 ) )
        | ( ( n5 = n5 )
          & ( n5 = n2 ) )
        | ( n4 != n5 )
        | ( n4 != n2 )
        | ~ leq(n0,n5)
        | ~ leq(n0,n2)
        | ~ leq(n5,n5) )
  <=> ( ( a_select2(xinit_noise,n4) = n0 )
      | ~ leq(n2,n5)
      | ( ( n0 = n5 )
        & ( n3 = n2 ) )
      | ( ( n0 = n5 )
        & ( n4 = n2 ) )
      | ( ( n0 = n5 )
        & ( n5 = n2 ) )
      | ( ( n0 = n2 )
        & ( n5 = n5 ) )
      | ( ( n1 = n5 )
        & ( n3 = n2 ) )
      | ( ( n1 = n5 )
        & ( n4 = n2 ) )
      | ( ( n1 = n5 )
        & ( n5 = n2 ) )
      | ( ( n1 = n2 )
        & ( n5 = n5 ) )
      | ( ( n2 = n5 )
        & ( n3 = n2 ) )
      | ( ( n2 = n5 )
        & ( n4 = n2 ) )
      | ( ( n2 = n5 )
        & ( n5 = n2 ) )
      | ( ( n2 = n2 )
        & ( n5 = n5 ) )
      | ( ( n3 = n5 )
        & ( n3 = n2 ) )
      | ( ( n3 = n5 )
        & ( n4 = n2 ) )
      | ( ( n3 = n5 )
        & ( n5 = n2 ) )
      | ( ( n3 = n2 )
        & ( n4 = n5 ) )
      | ( ( n3 = n2 )
        & ( n5 = n5 ) )
      | ( ( n4 = n5 )
        & ( n4 = n2 ) )
      | ( ( n4 = n5 )
        & ( n5 = n2 ) )
      | ( ( n4 = n2 )
        & ( n5 = n5 ) )
      | ( ( n5 = n5 )
        & ( n5 = n2 ) )
      | ( n4 != n5 )
      | ( n4 != n2 )
      | ~ leq(n0,n5)
      | ~ leq(n0,n2)
      | ~ leq(n5,n5) ) ),
    inference(elim_unused_vars,[status(thm)],[]) ).

tff(27,plain,
    ( ! [E: $i,F: $i] :
        ( ( a_select2(xinit_noise,n4) = n0 )
        | ~ ( leq(n0,E)
            & leq(n0,F)
            & leq(E,n5)
            & leq(F,n5) )
        | ~ ( ~ ( ( n0 = E )
                & ( n3 = F ) )
            & ~ ( ( n0 = E )
                & ( n4 = F ) )
            & ~ ( ( n0 = E )
                & ( n5 = F ) )
            & ~ ( ( n0 = F )
                & ( n5 = E ) )
            & ~ ( ( n1 = E )
                & ( n3 = F ) )
            & ~ ( ( n1 = E )
                & ( n4 = F ) )
            & ~ ( ( n1 = E )
                & ( n5 = F ) )
            & ~ ( ( n1 = F )
                & ( n5 = E ) )
            & ~ ( ( n2 = E )
                & ( n3 = F ) )
            & ~ ( ( n2 = E )
                & ( n4 = F ) )
            & ~ ( ( n2 = E )
                & ( n5 = F ) )
            & ~ ( ( n2 = F )
                & ( n5 = E ) )
            & ~ ( ( n3 = E )
                & ( n3 = F ) )
            & ~ ( ( n3 = E )
                & ( n4 = F ) )
            & ~ ( ( n3 = E )
                & ( n5 = F ) )
            & ~ ( ( n3 = F )
                & ( n4 = E ) )
            & ~ ( ( n3 = F )
                & ( n5 = E ) )
            & ~ ( ( n4 = E )
                & ( n4 = F ) )
            & ~ ( ( n4 = E )
                & ( n5 = F ) )
            & ~ ( ( n4 = F )
                & ( n5 = E ) )
            & ~ ( ( n5 = E )
                & ( n5 = F ) )
            & ( n2 = F )
            & ( n4 = E )
            & ( n4 = F )
            & ( n5 = E ) ) )
  <=> ! [E: $i,F: $i] :
        ( ( a_select2(xinit_noise,n4) = n0 )
        | ~ leq(n2,n5)
        | ( ( n0 = n5 )
          & ( n3 = n2 ) )
        | ( ( n0 = n5 )
          & ( n4 = n2 ) )
        | ( ( n0 = n5 )
          & ( n5 = n2 ) )
        | ( ( n0 = n2 )
          & ( n5 = n5 ) )
        | ( ( n1 = n5 )
          & ( n3 = n2 ) )
        | ( ( n1 = n5 )
          & ( n4 = n2 ) )
        | ( ( n1 = n5 )
          & ( n5 = n2 ) )
        | ( ( n1 = n2 )
          & ( n5 = n5 ) )
        | ( ( n2 = n5 )
          & ( n3 = n2 ) )
        | ( ( n2 = n5 )
          & ( n4 = n2 ) )
        | ( ( n2 = n5 )
          & ( n5 = n2 ) )
        | ( ( n2 = n2 )
          & ( n5 = n5 ) )
        | ( ( n3 = n5 )
          & ( n3 = n2 ) )
        | ( ( n3 = n5 )
          & ( n4 = n2 ) )
        | ( ( n3 = n5 )
          & ( n5 = n2 ) )
        | ( ( n3 = n2 )
          & ( n4 = n5 ) )
        | ( ( n3 = n2 )
          & ( n5 = n5 ) )
        | ( ( n4 = n5 )
          & ( n4 = n2 ) )
        | ( ( n4 = n5 )
          & ( n5 = n2 ) )
        | ( ( n4 = n2 )
          & ( n5 = n5 ) )
        | ( ( n5 = n5 )
          & ( n5 = n2 ) )
        | ( n4 != n5 )
        | ( n4 != n2 )
        | ~ leq(n0,n5)
        | ~ leq(n0,n2)
        | ~ leq(n5,n5) ) ),
    inference(destructive_equality_resolution,[status(thm)],[]) ).

tff(28,plain,
    ( ! [E: $i,F: $i] :
        ( ( a_select2(xinit_noise,n4) = n0 )
        | ~ ( leq(n0,E)
            & leq(n0,F)
            & leq(E,n5)
            & leq(F,n5) )
        | ~ ( ~ ( ( n0 = E )
                & ( n3 = F ) )
            & ~ ( ( n0 = E )
                & ( n4 = F ) )
            & ~ ( ( n0 = E )
                & ( n5 = F ) )
            & ~ ( ( n0 = F )
                & ( n5 = E ) )
            & ~ ( ( n1 = E )
                & ( n3 = F ) )
            & ~ ( ( n1 = E )
                & ( n4 = F ) )
            & ~ ( ( n1 = E )
                & ( n5 = F ) )
            & ~ ( ( n1 = F )
                & ( n5 = E ) )
            & ~ ( ( n2 = E )
                & ( n3 = F ) )
            & ~ ( ( n2 = E )
                & ( n4 = F ) )
            & ~ ( ( n2 = E )
                & ( n5 = F ) )
            & ~ ( ( n2 = F )
                & ( n5 = E ) )
            & ~ ( ( n3 = E )
                & ( n3 = F ) )
            & ~ ( ( n3 = E )
                & ( n4 = F ) )
            & ~ ( ( n3 = E )
                & ( n5 = F ) )
            & ~ ( ( n3 = F )
                & ( n4 = E ) )
            & ~ ( ( n3 = F )
                & ( n5 = E ) )
            & ~ ( ( n4 = E )
                & ( n4 = F ) )
            & ~ ( ( n4 = E )
                & ( n5 = F ) )
            & ~ ( ( n4 = F )
                & ( n5 = E ) )
            & ~ ( ( n5 = E )
                & ( n5 = F ) )
            & ( n2 = F )
            & ( n4 = E )
            & ( n4 = F )
            & ( n5 = E ) ) )
  <=> ( ( a_select2(xinit_noise,n4) = n0 )
      | ~ leq(n2,n5)
      | ( ( n0 = n5 )
        & ( n3 = n2 ) )
      | ( ( n0 = n5 )
        & ( n4 = n2 ) )
      | ( ( n0 = n5 )
        & ( n5 = n2 ) )
      | ( ( n0 = n2 )
        & ( n5 = n5 ) )
      | ( ( n1 = n5 )
        & ( n3 = n2 ) )
      | ( ( n1 = n5 )
        & ( n4 = n2 ) )
      | ( ( n1 = n5 )
        & ( n5 = n2 ) )
      | ( ( n1 = n2 )
        & ( n5 = n5 ) )
      | ( ( n2 = n5 )
        & ( n3 = n2 ) )
      | ( ( n2 = n5 )
        & ( n4 = n2 ) )
      | ( ( n2 = n5 )
        & ( n5 = n2 ) )
      | ( ( n2 = n2 )
        & ( n5 = n5 ) )
      | ( ( n3 = n5 )
        & ( n3 = n2 ) )
      | ( ( n3 = n5 )
        & ( n4 = n2 ) )
      | ( ( n3 = n5 )
        & ( n5 = n2 ) )
      | ( ( n3 = n2 )
        & ( n4 = n5 ) )
      | ( ( n3 = n2 )
        & ( n5 = n5 ) )
      | ( ( n4 = n5 )
        & ( n4 = n2 ) )
      | ( ( n4 = n5 )
        & ( n5 = n2 ) )
      | ( ( n4 = n2 )
        & ( n5 = n5 ) )
      | ( ( n5 = n5 )
        & ( n5 = n2 ) )
      | ( n4 != n5 )
      | ( n4 != n2 )
      | ~ leq(n0,n5)
      | ~ leq(n0,n2)
      | ~ leq(n5,n5) ) ),
    inference(transitivity,[status(thm)],[27,26]) ).

tff(29,plain,
    ( ! [E: $i,F: $i] :
        ( ( a_select2(xinit_noise,n4) = n0 )
        | ~ ( leq(n0,E)
            & leq(n0,F)
            & leq(E,n5)
            & leq(F,n5) )
        | ~ ( ~ ( ( n0 = E )
                & ( n3 = F ) )
            & ~ ( ( n0 = E )
                & ( n4 = F ) )
            & ~ ( ( n0 = E )
                & ( n5 = F ) )
            & ~ ( ( n0 = F )
                & ( n5 = E ) )
            & ~ ( ( n1 = E )
                & ( n3 = F ) )
            & ~ ( ( n1 = E )
                & ( n4 = F ) )
            & ~ ( ( n1 = E )
                & ( n5 = F ) )
            & ~ ( ( n1 = F )
                & ( n5 = E ) )
            & ~ ( ( n2 = E )
                & ( n3 = F ) )
            & ~ ( ( n2 = E )
                & ( n4 = F ) )
            & ~ ( ( n2 = E )
                & ( n5 = F ) )
            & ~ ( ( n2 = F )
                & ( n5 = E ) )
            & ~ ( ( n3 = E )
                & ( n3 = F ) )
            & ~ ( ( n3 = E )
                & ( n4 = F ) )
            & ~ ( ( n3 = E )
                & ( n5 = F ) )
            & ~ ( ( n3 = F )
                & ( n4 = E ) )
            & ~ ( ( n3 = F )
                & ( n5 = E ) )
            & ~ ( ( n4 = E )
                & ( n4 = F ) )
            & ~ ( ( n4 = E )
                & ( n5 = F ) )
            & ~ ( ( n4 = F )
                & ( n5 = E ) )
            & ~ ( ( n5 = E )
                & ( n5 = F ) )
            & ( n2 = F )
            & ( n4 = E )
            & ( n4 = F )
            & ( n5 = E ) ) )
  <=> $true ),
    inference(transitivity,[status(thm)],[28,25]) ).

tff(30,plain,
    ^ [E: $i,F: $i] :
      trans(monotonicity(trans(monotonicity(rewrite(( ( leq(n0,E)
                  & leq(n0,F)
                  & leq(E,n5) )
              <=> ( leq(n0,E)
                  & leq(n0,F)
                  & leq(E,n5) ) )),
              ( ( leq(n0,E)
                & leq(n0,F)
                & leq(E,n5)
                & leq(F,n5) )
            <=> ( leq(n0,E)
                & leq(n0,F)
                & leq(E,n5)
                & leq(F,n5) ) )),
            rewrite(( ( leq(n0,E)
                & leq(n0,F)
                & leq(E,n5)
                & leq(F,n5) )
            <=> ( leq(n0,E)
                & leq(n0,F)
                & leq(E,n5)
                & leq(F,n5) ) )),
            ( ( leq(n0,E)
              & leq(n0,F)
              & leq(E,n5)
              & leq(F,n5) )
          <=> ( leq(n0,E)
              & leq(n0,F)
              & leq(E,n5)
              & leq(F,n5) ) )),
          trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite(( ( ~ ( ( n0 = E )
                                                                                                              & ( n3 = F ) )
                                                                                                          & ~ ( ( n0 = E )
                                                                                                              & ( n4 = F ) )
                                                                                                          & ~ ( ( n0 = E )
                                                                                                              & ( n5 = F ) ) )
                                                                                                      <=> ( ~ ( ( n0 = E )
                                                                                                              & ( n3 = F ) )
                                                                                                          & ~ ( ( n0 = E )
                                                                                                              & ( n4 = F ) )
                                                                                                          & ~ ( ( n0 = E )
                                                                                                              & ( n5 = F ) ) ) )),
                                                                                                      ( ( ~ ( ( n0 = E )
                                                                                                            & ( n3 = F ) )
                                                                                                        & ~ ( ( n0 = E )
                                                                                                            & ( n4 = F ) )
                                                                                                        & ~ ( ( n0 = E )
                                                                                                            & ( n5 = F ) )
                                                                                                        & ~ ( ( n0 = F )
                                                                                                            & ( n5 = E ) ) )
                                                                                                    <=> ( ~ ( ( n0 = E )
                                                                                                            & ( n3 = F ) )
                                                                                                        & ~ ( ( n0 = E )
                                                                                                            & ( n4 = F ) )
                                                                                                        & ~ ( ( n0 = E )
                                                                                                            & ( n5 = F ) )
                                                                                                        & ~ ( ( n0 = F )
                                                                                                            & ( n5 = E ) ) ) )),
                                                                                                    rewrite(( ( ~ ( ( n0 = E )
                                                                                                            & ( n3 = F ) )
                                                                                                        & ~ ( ( n0 = E )
                                                                                                            & ( n4 = F ) )
                                                                                                        & ~ ( ( n0 = E )
                                                                                                            & ( n5 = F ) )
                                                                                                        & ~ ( ( n0 = F )
                                                                                                            & ( n5 = E ) ) )
                                                                                                    <=> ( ~ ( ( n0 = E )
                                                                                                            & ( n3 = F ) )
                                                                                                        & ~ ( ( n0 = E )
                                                                                                            & ( n4 = F ) )
                                                                                                        & ~ ( ( n0 = E )
                                                                                                            & ( n5 = F ) )
                                                                                                        & ~ ( ( n0 = F )
                                                                                                            & ( n5 = E ) ) ) )),
                                                                                                    ( ( ~ ( ( n0 = E )
                                                                                                          & ( n3 = F ) )
                                                                                                      & ~ ( ( n0 = E )
                                                                                                          & ( n4 = F ) )
                                                                                                      & ~ ( ( n0 = E )
                                                                                                          & ( n5 = F ) )
                                                                                                      & ~ ( ( n0 = F )
                                                                                                          & ( n5 = E ) ) )
                                                                                                  <=> ( ~ ( ( n0 = E )
                                                                                                          & ( n3 = F ) )
                                                                                                      & ~ ( ( n0 = E )
                                                                                                          & ( n4 = F ) )
                                                                                                      & ~ ( ( n0 = E )
                                                                                                          & ( n5 = F ) )
                                                                                                      & ~ ( ( n0 = F )
                                                                                                          & ( n5 = E ) ) ) )),
                                                                                                  ( ( ~ ( ( n0 = E )
                                                                                                        & ( n3 = F ) )
                                                                                                    & ~ ( ( n0 = E )
                                                                                                        & ( n4 = F ) )
                                                                                                    & ~ ( ( n0 = E )
                                                                                                        & ( n5 = F ) )
                                                                                                    & ~ ( ( n0 = F )
                                                                                                        & ( n5 = E ) )
                                                                                                    & ~ ( ( n1 = E )
                                                                                                        & ( n3 = F ) ) )
                                                                                                <=> ( ~ ( ( n0 = E )
                                                                                                        & ( n3 = F ) )
                                                                                                    & ~ ( ( n0 = E )
                                                                                                        & ( n4 = F ) )
                                                                                                    & ~ ( ( n0 = E )
                                                                                                        & ( n5 = F ) )
                                                                                                    & ~ ( ( n0 = F )
                                                                                                        & ( n5 = E ) )
                                                                                                    & ~ ( ( n1 = E )
                                                                                                        & ( n3 = F ) ) ) )),
                                                                                                rewrite(( ( ~ ( ( n0 = E )
                                                                                                        & ( n3 = F ) )
                                                                                                    & ~ ( ( n0 = E )
                                                                                                        & ( n4 = F ) )
                                                                                                    & ~ ( ( n0 = E )
                                                                                                        & ( n5 = F ) )
                                                                                                    & ~ ( ( n0 = F )
                                                                                                        & ( n5 = E ) )
                                                                                                    & ~ ( ( n1 = E )
                                                                                                        & ( n3 = F ) ) )
                                                                                                <=> ( ~ ( ( n0 = E )
                                                                                                        & ( n3 = F ) )
                                                                                                    & ~ ( ( n0 = E )
                                                                                                        & ( n4 = F ) )
                                                                                                    & ~ ( ( n0 = E )
                                                                                                        & ( n5 = F ) )
                                                                                                    & ~ ( ( n0 = F )
                                                                                                        & ( n5 = E ) )
                                                                                                    & ~ ( ( n1 = E )
                                                                                                        & ( n3 = F ) ) ) )),
                                                                                                ( ( ~ ( ( n0 = E )
                                                                                                      & ( n3 = F ) )
                                                                                                  & ~ ( ( n0 = E )
                                                                                                      & ( n4 = F ) )
                                                                                                  & ~ ( ( n0 = E )
                                                                                                      & ( n5 = F ) )
                                                                                                  & ~ ( ( n0 = F )
                                                                                                      & ( n5 = E ) )
                                                                                                  & ~ ( ( n1 = E )
                                                                                                      & ( n3 = F ) ) )
                                                                                              <=> ( ~ ( ( n0 = E )
                                                                                                      & ( n3 = F ) )
                                                                                                  & ~ ( ( n0 = E )
                                                                                                      & ( n4 = F ) )
                                                                                                  & ~ ( ( n0 = E )
                                                                                                      & ( n5 = F ) )
                                                                                                  & ~ ( ( n0 = F )
                                                                                                      & ( n5 = E ) )
                                                                                                  & ~ ( ( n1 = E )
                                                                                                      & ( n3 = F ) ) ) )),
                                                                                              ( ( ~ ( ( n0 = E )
                                                                                                    & ( n3 = F ) )
                                                                                                & ~ ( ( n0 = E )
                                                                                                    & ( n4 = F ) )
                                                                                                & ~ ( ( n0 = E )
                                                                                                    & ( n5 = F ) )
                                                                                                & ~ ( ( n0 = F )
                                                                                                    & ( n5 = E ) )
                                                                                                & ~ ( ( n1 = E )
                                                                                                    & ( n3 = F ) )
                                                                                                & ~ ( ( n1 = E )
                                                                                                    & ( n4 = F ) ) )
                                                                                            <=> ( ~ ( ( n0 = E )
                                                                                                    & ( n3 = F ) )
                                                                                                & ~ ( ( n0 = E )
                                                                                                    & ( n4 = F ) )
                                                                                                & ~ ( ( n0 = E )
                                                                                                    & ( n5 = F ) )
                                                                                                & ~ ( ( n0 = F )
                                                                                                    & ( n5 = E ) )
                                                                                                & ~ ( ( n1 = E )
                                                                                                    & ( n3 = F ) )
                                                                                                & ~ ( ( n1 = E )
                                                                                                    & ( n4 = F ) ) ) )),
                                                                                            rewrite(( ( ~ ( ( n0 = E )
                                                                                                    & ( n3 = F ) )
                                                                                                & ~ ( ( n0 = E )
                                                                                                    & ( n4 = F ) )
                                                                                                & ~ ( ( n0 = E )
                                                                                                    & ( n5 = F ) )
                                                                                                & ~ ( ( n0 = F )
                                                                                                    & ( n5 = E ) )
                                                                                                & ~ ( ( n1 = E )
                                                                                                    & ( n3 = F ) )
                                                                                                & ~ ( ( n1 = E )
                                                                                                    & ( n4 = F ) ) )
                                                                                            <=> ( ~ ( ( n0 = E )
                                                                                                    & ( n3 = F ) )
                                                                                                & ~ ( ( n0 = E )
                                                                                                    & ( n4 = F ) )
                                                                                                & ~ ( ( n0 = E )
                                                                                                    & ( n5 = F ) )
                                                                                                & ~ ( ( n0 = F )
                                                                                                    & ( n5 = E ) )
                                                                                                & ~ ( ( n1 = E )
                                                                                                    & ( n3 = F ) )
                                                                                                & ~ ( ( n1 = E )
                                                                                                    & ( n4 = F ) ) ) )),
                                                                                            ( ( ~ ( ( n0 = E )
                                                                                                  & ( n3 = F ) )
                                                                                              & ~ ( ( n0 = E )
                                                                                                  & ( n4 = F ) )
                                                                                              & ~ ( ( n0 = E )
                                                                                                  & ( n5 = F ) )
                                                                                              & ~ ( ( n0 = F )
                                                                                                  & ( n5 = E ) )
                                                                                              & ~ ( ( n1 = E )
                                                                                                  & ( n3 = F ) )
                                                                                              & ~ ( ( n1 = E )
                                                                                                  & ( n4 = F ) ) )
                                                                                          <=> ( ~ ( ( n0 = E )
                                                                                                  & ( n3 = F ) )
                                                                                              & ~ ( ( n0 = E )
                                                                                                  & ( n4 = F ) )
                                                                                              & ~ ( ( n0 = E )
                                                                                                  & ( n5 = F ) )
                                                                                              & ~ ( ( n0 = F )
                                                                                                  & ( n5 = E ) )
                                                                                              & ~ ( ( n1 = E )
                                                                                                  & ( n3 = F ) )
                                                                                              & ~ ( ( n1 = E )
                                                                                                  & ( n4 = F ) ) ) )),
                                                                                          ( ( ~ ( ( n0 = E )
                                                                                                & ( n3 = F ) )
                                                                                            & ~ ( ( n0 = E )
                                                                                                & ( n4 = F ) )
                                                                                            & ~ ( ( n0 = E )
                                                                                                & ( n5 = F ) )
                                                                                            & ~ ( ( n0 = F )
                                                                                                & ( n5 = E ) )
                                                                                            & ~ ( ( n1 = E )
                                                                                                & ( n3 = F ) )
                                                                                            & ~ ( ( n1 = E )
                                                                                                & ( n4 = F ) )
                                                                                            & ~ ( ( n1 = E )
                                                                                                & ( n5 = F ) ) )
                                                                                        <=> ( ~ ( ( n0 = E )
                                                                                                & ( n3 = F ) )
                                                                                            & ~ ( ( n0 = E )
                                                                                                & ( n4 = F ) )
                                                                                            & ~ ( ( n0 = E )
                                                                                                & ( n5 = F ) )
                                                                                            & ~ ( ( n0 = F )
                                                                                                & ( n5 = E ) )
                                                                                            & ~ ( ( n1 = E )
                                                                                                & ( n3 = F ) )
                                                                                            & ~ ( ( n1 = E )
                                                                                                & ( n4 = F ) )
                                                                                            & ~ ( ( n1 = E )
                                                                                                & ( n5 = F ) ) ) )),
                                                                                        rewrite(( ( ~ ( ( n0 = E )
                                                                                                & ( n3 = F ) )
                                                                                            & ~ ( ( n0 = E )
                                                                                                & ( n4 = F ) )
                                                                                            & ~ ( ( n0 = E )
                                                                                                & ( n5 = F ) )
                                                                                            & ~ ( ( n0 = F )
                                                                                                & ( n5 = E ) )
                                                                                            & ~ ( ( n1 = E )
                                                                                                & ( n3 = F ) )
                                                                                            & ~ ( ( n1 = E )
                                                                                                & ( n4 = F ) )
                                                                                            & ~ ( ( n1 = E )
                                                                                                & ( n5 = F ) ) )
                                                                                        <=> ( ~ ( ( n0 = E )
                                                                                                & ( n3 = F ) )
                                                                                            & ~ ( ( n0 = E )
                                                                                                & ( n4 = F ) )
                                                                                            & ~ ( ( n0 = E )
                                                                                                & ( n5 = F ) )
                                                                                            & ~ ( ( n0 = F )
                                                                                                & ( n5 = E ) )
                                                                                            & ~ ( ( n1 = E )
                                                                                                & ( n3 = F ) )
                                                                                            & ~ ( ( n1 = E )
                                                                                                & ( n4 = F ) )
                                                                                            & ~ ( ( n1 = E )
                                                                                                & ( n5 = F ) ) ) )),
                                                                                        ( ( ~ ( ( n0 = E )
                                                                                              & ( n3 = F ) )
                                                                                          & ~ ( ( n0 = E )
                                                                                              & ( n4 = F ) )
                                                                                          & ~ ( ( n0 = E )
                                                                                              & ( n5 = F ) )
                                                                                          & ~ ( ( n0 = F )
                                                                                              & ( n5 = E ) )
                                                                                          & ~ ( ( n1 = E )
                                                                                              & ( n3 = F ) )
                                                                                          & ~ ( ( n1 = E )
                                                                                              & ( n4 = F ) )
                                                                                          & ~ ( ( n1 = E )
                                                                                              & ( n5 = F ) ) )
                                                                                      <=> ( ~ ( ( n0 = E )
                                                                                              & ( n3 = F ) )
                                                                                          & ~ ( ( n0 = E )
                                                                                              & ( n4 = F ) )
                                                                                          & ~ ( ( n0 = E )
                                                                                              & ( n5 = F ) )
                                                                                          & ~ ( ( n0 = F )
                                                                                              & ( n5 = E ) )
                                                                                          & ~ ( ( n1 = E )
                                                                                              & ( n3 = F ) )
                                                                                          & ~ ( ( n1 = E )
                                                                                              & ( n4 = F ) )
                                                                                          & ~ ( ( n1 = E )
                                                                                              & ( n5 = F ) ) ) )),
                                                                                      ( ( ~ ( ( n0 = E )
                                                                                            & ( n3 = F ) )
                                                                                        & ~ ( ( n0 = E )
                                                                                            & ( n4 = F ) )
                                                                                        & ~ ( ( n0 = E )
                                                                                            & ( n5 = F ) )
                                                                                        & ~ ( ( n0 = F )
                                                                                            & ( n5 = E ) )
                                                                                        & ~ ( ( n1 = E )
                                                                                            & ( n3 = F ) )
                                                                                        & ~ ( ( n1 = E )
                                                                                            & ( n4 = F ) )
                                                                                        & ~ ( ( n1 = E )
                                                                                            & ( n5 = F ) )
                                                                                        & ~ ( ( n1 = F )
                                                                                            & ( n5 = E ) ) )
                                                                                    <=> ( ~ ( ( n0 = E )
                                                                                            & ( n3 = F ) )
                                                                                        & ~ ( ( n0 = E )
                                                                                            & ( n4 = F ) )
                                                                                        & ~ ( ( n0 = E )
                                                                                            & ( n5 = F ) )
                                                                                        & ~ ( ( n0 = F )
                                                                                            & ( n5 = E ) )
                                                                                        & ~ ( ( n1 = E )
                                                                                            & ( n3 = F ) )
                                                                                        & ~ ( ( n1 = E )
                                                                                            & ( n4 = F ) )
                                                                                        & ~ ( ( n1 = E )
                                                                                            & ( n5 = F ) )
                                                                                        & ~ ( ( n1 = F )
                                                                                            & ( n5 = E ) ) ) )),
                                                                                    rewrite(( ( ~ ( ( n0 = E )
                                                                                            & ( n3 = F ) )
                                                                                        & ~ ( ( n0 = E )
                                                                                            & ( n4 = F ) )
                                                                                        & ~ ( ( n0 = E )
                                                                                            & ( n5 = F ) )
                                                                                        & ~ ( ( n0 = F )
                                                                                            & ( n5 = E ) )
                                                                                        & ~ ( ( n1 = E )
                                                                                            & ( n3 = F ) )
                                                                                        & ~ ( ( n1 = E )
                                                                                            & ( n4 = F ) )
                                                                                        & ~ ( ( n1 = E )
                                                                                            & ( n5 = F ) )
                                                                                        & ~ ( ( n1 = F )
                                                                                            & ( n5 = E ) ) )
                                                                                    <=> ( ~ ( ( n0 = E )
                                                                                            & ( n3 = F ) )
                                                                                        & ~ ( ( n0 = E )
                                                                                            & ( n4 = F ) )
                                                                                        & ~ ( ( n0 = E )
                                                                                            & ( n5 = F ) )
                                                                                        & ~ ( ( n0 = F )
                                                                                            & ( n5 = E ) )
                                                                                        & ~ ( ( n1 = E )
                                                                                            & ( n3 = F ) )
                                                                                        & ~ ( ( n1 = E )
                                                                                            & ( n4 = F ) )
                                                                                        & ~ ( ( n1 = E )
                                                                                            & ( n5 = F ) )
                                                                                        & ~ ( ( n1 = F )
                                                                                            & ( n5 = E ) ) ) )),
                                                                                    ( ( ~ ( ( n0 = E )
                                                                                          & ( n3 = F ) )
                                                                                      & ~ ( ( n0 = E )
                                                                                          & ( n4 = F ) )
                                                                                      & ~ ( ( n0 = E )
                                                                                          & ( n5 = F ) )
                                                                                      & ~ ( ( n0 = F )
                                                                                          & ( n5 = E ) )
                                                                                      & ~ ( ( n1 = E )
                                                                                          & ( n3 = F ) )
                                                                                      & ~ ( ( n1 = E )
                                                                                          & ( n4 = F ) )
                                                                                      & ~ ( ( n1 = E )
                                                                                          & ( n5 = F ) )
                                                                                      & ~ ( ( n1 = F )
                                                                                          & ( n5 = E ) ) )
                                                                                  <=> ( ~ ( ( n0 = E )
                                                                                          & ( n3 = F ) )
                                                                                      & ~ ( ( n0 = E )
                                                                                          & ( n4 = F ) )
                                                                                      & ~ ( ( n0 = E )
                                                                                          & ( n5 = F ) )
                                                                                      & ~ ( ( n0 = F )
                                                                                          & ( n5 = E ) )
                                                                                      & ~ ( ( n1 = E )
                                                                                          & ( n3 = F ) )
                                                                                      & ~ ( ( n1 = E )
                                                                                          & ( n4 = F ) )
                                                                                      & ~ ( ( n1 = E )
                                                                                          & ( n5 = F ) )
                                                                                      & ~ ( ( n1 = F )
                                                                                          & ( n5 = E ) ) ) )),
                                                                                  ( ( ~ ( ( n0 = E )
                                                                                        & ( n3 = F ) )
                                                                                    & ~ ( ( n0 = E )
                                                                                        & ( n4 = F ) )
                                                                                    & ~ ( ( n0 = E )
                                                                                        & ( n5 = F ) )
                                                                                    & ~ ( ( n0 = F )
                                                                                        & ( n5 = E ) )
                                                                                    & ~ ( ( n1 = E )
                                                                                        & ( n3 = F ) )
                                                                                    & ~ ( ( n1 = E )
                                                                                        & ( n4 = F ) )
                                                                                    & ~ ( ( n1 = E )
                                                                                        & ( n5 = F ) )
                                                                                    & ~ ( ( n1 = F )
                                                                                        & ( n5 = E ) )
                                                                                    & ~ ( ( n2 = E )
                                                                                        & ( n3 = F ) ) )
                                                                                <=> ( ~ ( ( n0 = E )
                                                                                        & ( n3 = F ) )
                                                                                    & ~ ( ( n0 = E )
                                                                                        & ( n4 = F ) )
                                                                                    & ~ ( ( n0 = E )
                                                                                        & ( n5 = F ) )
                                                                                    & ~ ( ( n0 = F )
                                                                                        & ( n5 = E ) )
                                                                                    & ~ ( ( n1 = E )
                                                                                        & ( n3 = F ) )
                                                                                    & ~ ( ( n1 = E )
                                                                                        & ( n4 = F ) )
                                                                                    & ~ ( ( n1 = E )
                                                                                        & ( n5 = F ) )
                                                                                    & ~ ( ( n1 = F )
                                                                                        & ( n5 = E ) )
                                                                                    & ~ ( ( n2 = E )
                                                                                        & ( n3 = F ) ) ) )),
                                                                                rewrite(( ( ~ ( ( n0 = E )
                                                                                        & ( n3 = F ) )
                                                                                    & ~ ( ( n0 = E )
                                                                                        & ( n4 = F ) )
                                                                                    & ~ ( ( n0 = E )
                                                                                        & ( n5 = F ) )
                                                                                    & ~ ( ( n0 = F )
                                                                                        & ( n5 = E ) )
                                                                                    & ~ ( ( n1 = E )
                                                                                        & ( n3 = F ) )
                                                                                    & ~ ( ( n1 = E )
                                                                                        & ( n4 = F ) )
                                                                                    & ~ ( ( n1 = E )
                                                                                        & ( n5 = F ) )
                                                                                    & ~ ( ( n1 = F )
                                                                                        & ( n5 = E ) )
                                                                                    & ~ ( ( n2 = E )
                                                                                        & ( n3 = F ) ) )
                                                                                <=> ( ~ ( ( n0 = E )
                                                                                        & ( n3 = F ) )
                                                                                    & ~ ( ( n0 = E )
                                                                                        & ( n4 = F ) )
                                                                                    & ~ ( ( n0 = E )
                                                                                        & ( n5 = F ) )
                                                                                    & ~ ( ( n0 = F )
                                                                                        & ( n5 = E ) )
                                                                                    & ~ ( ( n1 = E )
                                                                                        & ( n3 = F ) )
                                                                                    & ~ ( ( n1 = E )
                                                                                        & ( n4 = F ) )
                                                                                    & ~ ( ( n1 = E )
                                                                                        & ( n5 = F ) )
                                                                                    & ~ ( ( n1 = F )
                                                                                        & ( n5 = E ) )
                                                                                    & ~ ( ( n2 = E )
                                                                                        & ( n3 = F ) ) ) )),
                                                                                ( ( ~ ( ( n0 = E )
                                                                                      & ( n3 = F ) )
                                                                                  & ~ ( ( n0 = E )
                                                                                      & ( n4 = F ) )
                                                                                  & ~ ( ( n0 = E )
                                                                                      & ( n5 = F ) )
                                                                                  & ~ ( ( n0 = F )
                                                                                      & ( n5 = E ) )
                                                                                  & ~ ( ( n1 = E )
                                                                                      & ( n3 = F ) )
                                                                                  & ~ ( ( n1 = E )
                                                                                      & ( n4 = F ) )
                                                                                  & ~ ( ( n1 = E )
                                                                                      & ( n5 = F ) )
                                                                                  & ~ ( ( n1 = F )
                                                                                      & ( n5 = E ) )
                                                                                  & ~ ( ( n2 = E )
                                                                                      & ( n3 = F ) ) )
                                                                              <=> ( ~ ( ( n0 = E )
                                                                                      & ( n3 = F ) )
                                                                                  & ~ ( ( n0 = E )
                                                                                      & ( n4 = F ) )
                                                                                  & ~ ( ( n0 = E )
                                                                                      & ( n5 = F ) )
                                                                                  & ~ ( ( n0 = F )
                                                                                      & ( n5 = E ) )
                                                                                  & ~ ( ( n1 = E )
                                                                                      & ( n3 = F ) )
                                                                                  & ~ ( ( n1 = E )
                                                                                      & ( n4 = F ) )
                                                                                  & ~ ( ( n1 = E )
                                                                                      & ( n5 = F ) )
                                                                                  & ~ ( ( n1 = F )
                                                                                      & ( n5 = E ) )
                                                                                  & ~ ( ( n2 = E )
                                                                                      & ( n3 = F ) ) ) )),
                                                                              ( ( ~ ( ( n0 = E )
                                                                                    & ( n3 = F ) )
                                                                                & ~ ( ( n0 = E )
                                                                                    & ( n4 = F ) )
                                                                                & ~ ( ( n0 = E )
                                                                                    & ( n5 = F ) )
                                                                                & ~ ( ( n0 = F )
                                                                                    & ( n5 = E ) )
                                                                                & ~ ( ( n1 = E )
                                                                                    & ( n3 = F ) )
                                                                                & ~ ( ( n1 = E )
                                                                                    & ( n4 = F ) )
                                                                                & ~ ( ( n1 = E )
                                                                                    & ( n5 = F ) )
                                                                                & ~ ( ( n1 = F )
                                                                                    & ( n5 = E ) )
                                                                                & ~ ( ( n2 = E )
                                                                                    & ( n3 = F ) )
                                                                                & ~ ( ( n2 = E )
                                                                                    & ( n4 = F ) ) )
                                                                            <=> ( ~ ( ( n0 = E )
                                                                                    & ( n3 = F ) )
                                                                                & ~ ( ( n0 = E )
                                                                                    & ( n4 = F ) )
                                                                                & ~ ( ( n0 = E )
                                                                                    & ( n5 = F ) )
                                                                                & ~ ( ( n0 = F )
                                                                                    & ( n5 = E ) )
                                                                                & ~ ( ( n1 = E )
                                                                                    & ( n3 = F ) )
                                                                                & ~ ( ( n1 = E )
                                                                                    & ( n4 = F ) )
                                                                                & ~ ( ( n1 = E )
                                                                                    & ( n5 = F ) )
                                                                                & ~ ( ( n1 = F )
                                                                                    & ( n5 = E ) )
                                                                                & ~ ( ( n2 = E )
                                                                                    & ( n3 = F ) )
                                                                                & ~ ( ( n2 = E )
                                                                                    & ( n4 = F ) ) ) )),
                                                                            rewrite(( ( ~ ( ( n0 = E )
                                                                                    & ( n3 = F ) )
                                                                                & ~ ( ( n0 = E )
                                                                                    & ( n4 = F ) )
                                                                                & ~ ( ( n0 = E )
                                                                                    & ( n5 = F ) )
                                                                                & ~ ( ( n0 = F )
                                                                                    & ( n5 = E ) )
                                                                                & ~ ( ( n1 = E )
                                                                                    & ( n3 = F ) )
                                                                                & ~ ( ( n1 = E )
                                                                                    & ( n4 = F ) )
                                                                                & ~ ( ( n1 = E )
                                                                                    & ( n5 = F ) )
                                                                                & ~ ( ( n1 = F )
                                                                                    & ( n5 = E ) )
                                                                                & ~ ( ( n2 = E )
                                                                                    & ( n3 = F ) )
                                                                                & ~ ( ( n2 = E )
                                                                                    & ( n4 = F ) ) )
                                                                            <=> ( ~ ( ( n0 = E )
                                                                                    & ( n3 = F ) )
                                                                                & ~ ( ( n0 = E )
                                                                                    & ( n4 = F ) )
                                                                                & ~ ( ( n0 = E )
                                                                                    & ( n5 = F ) )
                                                                                & ~ ( ( n0 = F )
                                                                                    & ( n5 = E ) )
                                                                                & ~ ( ( n1 = E )
                                                                                    & ( n3 = F ) )
                                                                                & ~ ( ( n1 = E )
                                                                                    & ( n4 = F ) )
                                                                                & ~ ( ( n1 = E )
                                                                                    & ( n5 = F ) )
                                                                                & ~ ( ( n1 = F )
                                                                                    & ( n5 = E ) )
                                                                                & ~ ( ( n2 = E )
                                                                                    & ( n3 = F ) )
                                                                                & ~ ( ( n2 = E )
                                                                                    & ( n4 = F ) ) ) )),
                                                                            ( ( ~ ( ( n0 = E )
                                                                                  & ( n3 = F ) )
                                                                              & ~ ( ( n0 = E )
                                                                                  & ( n4 = F ) )
                                                                              & ~ ( ( n0 = E )
                                                                                  & ( n5 = F ) )
                                                                              & ~ ( ( n0 = F )
                                                                                  & ( n5 = E ) )
                                                                              & ~ ( ( n1 = E )
                                                                                  & ( n3 = F ) )
                                                                              & ~ ( ( n1 = E )
                                                                                  & ( n4 = F ) )
                                                                              & ~ ( ( n1 = E )
                                                                                  & ( n5 = F ) )
                                                                              & ~ ( ( n1 = F )
                                                                                  & ( n5 = E ) )
                                                                              & ~ ( ( n2 = E )
                                                                                  & ( n3 = F ) )
                                                                              & ~ ( ( n2 = E )
                                                                                  & ( n4 = F ) ) )
                                                                          <=> ( ~ ( ( n0 = E )
                                                                                  & ( n3 = F ) )
                                                                              & ~ ( ( n0 = E )
                                                                                  & ( n4 = F ) )
                                                                              & ~ ( ( n0 = E )
                                                                                  & ( n5 = F ) )
                                                                              & ~ ( ( n0 = F )
                                                                                  & ( n5 = E ) )
                                                                              & ~ ( ( n1 = E )
                                                                                  & ( n3 = F ) )
                                                                              & ~ ( ( n1 = E )
                                                                                  & ( n4 = F ) )
                                                                              & ~ ( ( n1 = E )
                                                                                  & ( n5 = F ) )
                                                                              & ~ ( ( n1 = F )
                                                                                  & ( n5 = E ) )
                                                                              & ~ ( ( n2 = E )
                                                                                  & ( n3 = F ) )
                                                                              & ~ ( ( n2 = E )
                                                                                  & ( n4 = F ) ) ) )),
                                                                          ( ( ~ ( ( n0 = E )
                                                                                & ( n3 = F ) )
                                                                            & ~ ( ( n0 = E )
                                                                                & ( n4 = F ) )
                                                                            & ~ ( ( n0 = E )
                                                                                & ( n5 = F ) )
                                                                            & ~ ( ( n0 = F )
                                                                                & ( n5 = E ) )
                                                                            & ~ ( ( n1 = E )
                                                                                & ( n3 = F ) )
                                                                            & ~ ( ( n1 = E )
                                                                                & ( n4 = F ) )
                                                                            & ~ ( ( n1 = E )
                                                                                & ( n5 = F ) )
                                                                            & ~ ( ( n1 = F )
                                                                                & ( n5 = E ) )
                                                                            & ~ ( ( n2 = E )
                                                                                & ( n3 = F ) )
                                                                            & ~ ( ( n2 = E )
                                                                                & ( n4 = F ) )
                                                                            & ~ ( ( n2 = E )
                                                                                & ( n5 = F ) ) )
                                                                        <=> ( ~ ( ( n0 = E )
                                                                                & ( n3 = F ) )
                                                                            & ~ ( ( n0 = E )
                                                                                & ( n4 = F ) )
                                                                            & ~ ( ( n0 = E )
                                                                                & ( n5 = F ) )
                                                                            & ~ ( ( n0 = F )
                                                                                & ( n5 = E ) )
                                                                            & ~ ( ( n1 = E )
                                                                                & ( n3 = F ) )
                                                                            & ~ ( ( n1 = E )
                                                                                & ( n4 = F ) )
                                                                            & ~ ( ( n1 = E )
                                                                                & ( n5 = F ) )
                                                                            & ~ ( ( n1 = F )
                                                                                & ( n5 = E ) )
                                                                            & ~ ( ( n2 = E )
                                                                                & ( n3 = F ) )
                                                                            & ~ ( ( n2 = E )
                                                                                & ( n4 = F ) )
                                                                            & ~ ( ( n2 = E )
                                                                                & ( n5 = F ) ) ) )),
                                                                        rewrite(( ( ~ ( ( n0 = E )
                                                                                & ( n3 = F ) )
                                                                            & ~ ( ( n0 = E )
                                                                                & ( n4 = F ) )
                                                                            & ~ ( ( n0 = E )
                                                                                & ( n5 = F ) )
                                                                            & ~ ( ( n0 = F )
                                                                                & ( n5 = E ) )
                                                                            & ~ ( ( n1 = E )
                                                                                & ( n3 = F ) )
                                                                            & ~ ( ( n1 = E )
                                                                                & ( n4 = F ) )
                                                                            & ~ ( ( n1 = E )
                                                                                & ( n5 = F ) )
                                                                            & ~ ( ( n1 = F )
                                                                                & ( n5 = E ) )
                                                                            & ~ ( ( n2 = E )
                                                                                & ( n3 = F ) )
                                                                            & ~ ( ( n2 = E )
                                                                                & ( n4 = F ) )
                                                                            & ~ ( ( n2 = E )
                                                                                & ( n5 = F ) ) )
                                                                        <=> ( ~ ( ( n0 = E )
                                                                                & ( n3 = F ) )
                                                                            & ~ ( ( n0 = E )
                                                                                & ( n4 = F ) )
                                                                            & ~ ( ( n0 = E )
                                                                                & ( n5 = F ) )
                                                                            & ~ ( ( n0 = F )
                                                                                & ( n5 = E ) )
                                                                            & ~ ( ( n1 = E )
                                                                                & ( n3 = F ) )
                                                                            & ~ ( ( n1 = E )
                                                                                & ( n4 = F ) )
                                                                            & ~ ( ( n1 = E )
                                                                                & ( n5 = F ) )
                                                                            & ~ ( ( n1 = F )
                                                                                & ( n5 = E ) )
                                                                            & ~ ( ( n2 = E )
                                                                                & ( n3 = F ) )
                                                                            & ~ ( ( n2 = E )
                                                                                & ( n4 = F ) )
                                                                            & ~ ( ( n2 = E )
                                                                                & ( n5 = F ) ) ) )),
                                                                        ( ( ~ ( ( n0 = E )
                                                                              & ( n3 = F ) )
                                                                          & ~ ( ( n0 = E )
                                                                              & ( n4 = F ) )
                                                                          & ~ ( ( n0 = E )
                                                                              & ( n5 = F ) )
                                                                          & ~ ( ( n0 = F )
                                                                              & ( n5 = E ) )
                                                                          & ~ ( ( n1 = E )
                                                                              & ( n3 = F ) )
                                                                          & ~ ( ( n1 = E )
                                                                              & ( n4 = F ) )
                                                                          & ~ ( ( n1 = E )
                                                                              & ( n5 = F ) )
                                                                          & ~ ( ( n1 = F )
                                                                              & ( n5 = E ) )
                                                                          & ~ ( ( n2 = E )
                                                                              & ( n3 = F ) )
                                                                          & ~ ( ( n2 = E )
                                                                              & ( n4 = F ) )
                                                                          & ~ ( ( n2 = E )
                                                                              & ( n5 = F ) ) )
                                                                      <=> ( ~ ( ( n0 = E )
                                                                              & ( n3 = F ) )
                                                                          & ~ ( ( n0 = E )
                                                                              & ( n4 = F ) )
                                                                          & ~ ( ( n0 = E )
                                                                              & ( n5 = F ) )
                                                                          & ~ ( ( n0 = F )
                                                                              & ( n5 = E ) )
                                                                          & ~ ( ( n1 = E )
                                                                              & ( n3 = F ) )
                                                                          & ~ ( ( n1 = E )
                                                                              & ( n4 = F ) )
                                                                          & ~ ( ( n1 = E )
                                                                              & ( n5 = F ) )
                                                                          & ~ ( ( n1 = F )
                                                                              & ( n5 = E ) )
                                                                          & ~ ( ( n2 = E )
                                                                              & ( n3 = F ) )
                                                                          & ~ ( ( n2 = E )
                                                                              & ( n4 = F ) )
                                                                          & ~ ( ( n2 = E )
                                                                              & ( n5 = F ) ) ) )),
                                                                      ( ( ~ ( ( n0 = E )
                                                                            & ( n3 = F ) )
                                                                        & ~ ( ( n0 = E )
                                                                            & ( n4 = F ) )
                                                                        & ~ ( ( n0 = E )
                                                                            & ( n5 = F ) )
                                                                        & ~ ( ( n0 = F )
                                                                            & ( n5 = E ) )
                                                                        & ~ ( ( n1 = E )
                                                                            & ( n3 = F ) )
                                                                        & ~ ( ( n1 = E )
                                                                            & ( n4 = F ) )
                                                                        & ~ ( ( n1 = E )
                                                                            & ( n5 = F ) )
                                                                        & ~ ( ( n1 = F )
                                                                            & ( n5 = E ) )
                                                                        & ~ ( ( n2 = E )
                                                                            & ( n3 = F ) )
                                                                        & ~ ( ( n2 = E )
                                                                            & ( n4 = F ) )
                                                                        & ~ ( ( n2 = E )
                                                                            & ( n5 = F ) )
                                                                        & ~ ( ( n2 = F )
                                                                            & ( n5 = E ) ) )
                                                                    <=> ( ~ ( ( n0 = E )
                                                                            & ( n3 = F ) )
                                                                        & ~ ( ( n0 = E )
                                                                            & ( n4 = F ) )
                                                                        & ~ ( ( n0 = E )
                                                                            & ( n5 = F ) )
                                                                        & ~ ( ( n0 = F )
                                                                            & ( n5 = E ) )
                                                                        & ~ ( ( n1 = E )
                                                                            & ( n3 = F ) )
                                                                        & ~ ( ( n1 = E )
                                                                            & ( n4 = F ) )
                                                                        & ~ ( ( n1 = E )
                                                                            & ( n5 = F ) )
                                                                        & ~ ( ( n1 = F )
                                                                            & ( n5 = E ) )
                                                                        & ~ ( ( n2 = E )
                                                                            & ( n3 = F ) )
                                                                        & ~ ( ( n2 = E )
                                                                            & ( n4 = F ) )
                                                                        & ~ ( ( n2 = E )
                                                                            & ( n5 = F ) )
                                                                        & ~ ( ( n2 = F )
                                                                            & ( n5 = E ) ) ) )),
                                                                    rewrite(( ( ~ ( ( n0 = E )
                                                                            & ( n3 = F ) )
                                                                        & ~ ( ( n0 = E )
                                                                            & ( n4 = F ) )
                                                                        & ~ ( ( n0 = E )
                                                                            & ( n5 = F ) )
                                                                        & ~ ( ( n0 = F )
                                                                            & ( n5 = E ) )
                                                                        & ~ ( ( n1 = E )
                                                                            & ( n3 = F ) )
                                                                        & ~ ( ( n1 = E )
                                                                            & ( n4 = F ) )
                                                                        & ~ ( ( n1 = E )
                                                                            & ( n5 = F ) )
                                                                        & ~ ( ( n1 = F )
                                                                            & ( n5 = E ) )
                                                                        & ~ ( ( n2 = E )
                                                                            & ( n3 = F ) )
                                                                        & ~ ( ( n2 = E )
                                                                            & ( n4 = F ) )
                                                                        & ~ ( ( n2 = E )
                                                                            & ( n5 = F ) )
                                                                        & ~ ( ( n2 = F )
                                                                            & ( n5 = E ) ) )
                                                                    <=> ( ~ ( ( n0 = E )
                                                                            & ( n3 = F ) )
                                                                        & ~ ( ( n0 = E )
                                                                            & ( n4 = F ) )
                                                                        & ~ ( ( n0 = E )
                                                                            & ( n5 = F ) )
                                                                        & ~ ( ( n0 = F )
                                                                            & ( n5 = E ) )
                                                                        & ~ ( ( n1 = E )
                                                                            & ( n3 = F ) )
                                                                        & ~ ( ( n1 = E )
                                                                            & ( n4 = F ) )
                                                                        & ~ ( ( n1 = E )
                                                                            & ( n5 = F ) )
                                                                        & ~ ( ( n1 = F )
                                                                            & ( n5 = E ) )
                                                                        & ~ ( ( n2 = E )
                                                                            & ( n3 = F ) )
                                                                        & ~ ( ( n2 = E )
                                                                            & ( n4 = F ) )
                                                                        & ~ ( ( n2 = E )
                                                                            & ( n5 = F ) )
                                                                        & ~ ( ( n2 = F )
                                                                            & ( n5 = E ) ) ) )),
                                                                    ( ( ~ ( ( n0 = E )
                                                                          & ( n3 = F ) )
                                                                      & ~ ( ( n0 = E )
                                                                          & ( n4 = F ) )
                                                                      & ~ ( ( n0 = E )
                                                                          & ( n5 = F ) )
                                                                      & ~ ( ( n0 = F )
                                                                          & ( n5 = E ) )
                                                                      & ~ ( ( n1 = E )
                                                                          & ( n3 = F ) )
                                                                      & ~ ( ( n1 = E )
                                                                          & ( n4 = F ) )
                                                                      & ~ ( ( n1 = E )
                                                                          & ( n5 = F ) )
                                                                      & ~ ( ( n1 = F )
                                                                          & ( n5 = E ) )
                                                                      & ~ ( ( n2 = E )
                                                                          & ( n3 = F ) )
                                                                      & ~ ( ( n2 = E )
                                                                          & ( n4 = F ) )
                                                                      & ~ ( ( n2 = E )
                                                                          & ( n5 = F ) )
                                                                      & ~ ( ( n2 = F )
                                                                          & ( n5 = E ) ) )
                                                                  <=> ( ~ ( ( n0 = E )
                                                                          & ( n3 = F ) )
                                                                      & ~ ( ( n0 = E )
                                                                          & ( n4 = F ) )
                                                                      & ~ ( ( n0 = E )
                                                                          & ( n5 = F ) )
                                                                      & ~ ( ( n0 = F )
                                                                          & ( n5 = E ) )
                                                                      & ~ ( ( n1 = E )
                                                                          & ( n3 = F ) )
                                                                      & ~ ( ( n1 = E )
                                                                          & ( n4 = F ) )
                                                                      & ~ ( ( n1 = E )
                                                                          & ( n5 = F ) )
                                                                      & ~ ( ( n1 = F )
                                                                          & ( n5 = E ) )
                                                                      & ~ ( ( n2 = E )
                                                                          & ( n3 = F ) )
                                                                      & ~ ( ( n2 = E )
                                                                          & ( n4 = F ) )
                                                                      & ~ ( ( n2 = E )
                                                                          & ( n5 = F ) )
                                                                      & ~ ( ( n2 = F )
                                                                          & ( n5 = E ) ) ) )),
                                                                  ( ( ~ ( ( n0 = E )
                                                                        & ( n3 = F ) )
                                                                    & ~ ( ( n0 = E )
                                                                        & ( n4 = F ) )
                                                                    & ~ ( ( n0 = E )
                                                                        & ( n5 = F ) )
                                                                    & ~ ( ( n0 = F )
                                                                        & ( n5 = E ) )
                                                                    & ~ ( ( n1 = E )
                                                                        & ( n3 = F ) )
                                                                    & ~ ( ( n1 = E )
                                                                        & ( n4 = F ) )
                                                                    & ~ ( ( n1 = E )
                                                                        & ( n5 = F ) )
                                                                    & ~ ( ( n1 = F )
                                                                        & ( n5 = E ) )
                                                                    & ~ ( ( n2 = E )
                                                                        & ( n3 = F ) )
                                                                    & ~ ( ( n2 = E )
                                                                        & ( n4 = F ) )
                                                                    & ~ ( ( n2 = E )
                                                                        & ( n5 = F ) )
                                                                    & ~ ( ( n2 = F )
                                                                        & ( n5 = E ) )
                                                                    & ~ ( ( n3 = E )
                                                                        & ( n3 = F ) ) )
                                                                <=> ( ~ ( ( n0 = E )
                                                                        & ( n3 = F ) )
                                                                    & ~ ( ( n0 = E )
                                                                        & ( n4 = F ) )
                                                                    & ~ ( ( n0 = E )
                                                                        & ( n5 = F ) )
                                                                    & ~ ( ( n0 = F )
                                                                        & ( n5 = E ) )
                                                                    & ~ ( ( n1 = E )
                                                                        & ( n3 = F ) )
                                                                    & ~ ( ( n1 = E )
                                                                        & ( n4 = F ) )
                                                                    & ~ ( ( n1 = E )
                                                                        & ( n5 = F ) )
                                                                    & ~ ( ( n1 = F )
                                                                        & ( n5 = E ) )
                                                                    & ~ ( ( n2 = E )
                                                                        & ( n3 = F ) )
                                                                    & ~ ( ( n2 = E )
                                                                        & ( n4 = F ) )
                                                                    & ~ ( ( n2 = E )
                                                                        & ( n5 = F ) )
                                                                    & ~ ( ( n2 = F )
                                                                        & ( n5 = E ) )
                                                                    & ~ ( ( n3 = E )
                                                                        & ( n3 = F ) ) ) )),
                                                                rewrite(( ( ~ ( ( n0 = E )
                                                                        & ( n3 = F ) )
                                                                    & ~ ( ( n0 = E )
                                                                        & ( n4 = F ) )
                                                                    & ~ ( ( n0 = E )
                                                                        & ( n5 = F ) )
                                                                    & ~ ( ( n0 = F )
                                                                        & ( n5 = E ) )
                                                                    & ~ ( ( n1 = E )
                                                                        & ( n3 = F ) )
                                                                    & ~ ( ( n1 = E )
                                                                        & ( n4 = F ) )
                                                                    & ~ ( ( n1 = E )
                                                                        & ( n5 = F ) )
                                                                    & ~ ( ( n1 = F )
                                                                        & ( n5 = E ) )
                                                                    & ~ ( ( n2 = E )
                                                                        & ( n3 = F ) )
                                                                    & ~ ( ( n2 = E )
                                                                        & ( n4 = F ) )
                                                                    & ~ ( ( n2 = E )
                                                                        & ( n5 = F ) )
                                                                    & ~ ( ( n2 = F )
                                                                        & ( n5 = E ) )
                                                                    & ~ ( ( n3 = E )
                                                                        & ( n3 = F ) ) )
                                                                <=> ( ~ ( ( n0 = E )
                                                                        & ( n3 = F ) )
                                                                    & ~ ( ( n0 = E )
                                                                        & ( n4 = F ) )
                                                                    & ~ ( ( n0 = E )
                                                                        & ( n5 = F ) )
                                                                    & ~ ( ( n0 = F )
                                                                        & ( n5 = E ) )
                                                                    & ~ ( ( n1 = E )
                                                                        & ( n3 = F ) )
                                                                    & ~ ( ( n1 = E )
                                                                        & ( n4 = F ) )
                                                                    & ~ ( ( n1 = E )
                                                                        & ( n5 = F ) )
                                                                    & ~ ( ( n1 = F )
                                                                        & ( n5 = E ) )
                                                                    & ~ ( ( n2 = E )
                                                                        & ( n3 = F ) )
                                                                    & ~ ( ( n2 = E )
                                                                        & ( n4 = F ) )
                                                                    & ~ ( ( n2 = E )
                                                                        & ( n5 = F ) )
                                                                    & ~ ( ( n2 = F )
                                                                        & ( n5 = E ) )
                                                                    & ~ ( ( n3 = E )
                                                                        & ( n3 = F ) ) ) )),
                                                                ( ( ~ ( ( n0 = E )
                                                                      & ( n3 = F ) )
                                                                  & ~ ( ( n0 = E )
                                                                      & ( n4 = F ) )
                                                                  & ~ ( ( n0 = E )
                                                                      & ( n5 = F ) )
                                                                  & ~ ( ( n0 = F )
                                                                      & ( n5 = E ) )
                                                                  & ~ ( ( n1 = E )
                                                                      & ( n3 = F ) )
                                                                  & ~ ( ( n1 = E )
                                                                      & ( n4 = F ) )
                                                                  & ~ ( ( n1 = E )
                                                                      & ( n5 = F ) )
                                                                  & ~ ( ( n1 = F )
                                                                      & ( n5 = E ) )
                                                                  & ~ ( ( n2 = E )
                                                                      & ( n3 = F ) )
                                                                  & ~ ( ( n2 = E )
                                                                      & ( n4 = F ) )
                                                                  & ~ ( ( n2 = E )
                                                                      & ( n5 = F ) )
                                                                  & ~ ( ( n2 = F )
                                                                      & ( n5 = E ) )
                                                                  & ~ ( ( n3 = E )
                                                                      & ( n3 = F ) ) )
                                                              <=> ( ~ ( ( n0 = E )
                                                                      & ( n3 = F ) )
                                                                  & ~ ( ( n0 = E )
                                                                      & ( n4 = F ) )
                                                                  & ~ ( ( n0 = E )
                                                                      & ( n5 = F ) )
                                                                  & ~ ( ( n0 = F )
                                                                      & ( n5 = E ) )
                                                                  & ~ ( ( n1 = E )
                                                                      & ( n3 = F ) )
                                                                  & ~ ( ( n1 = E )
                                                                      & ( n4 = F ) )
                                                                  & ~ ( ( n1 = E )
                                                                      & ( n5 = F ) )
                                                                  & ~ ( ( n1 = F )
                                                                      & ( n5 = E ) )
                                                                  & ~ ( ( n2 = E )
                                                                      & ( n3 = F ) )
                                                                  & ~ ( ( n2 = E )
                                                                      & ( n4 = F ) )
                                                                  & ~ ( ( n2 = E )
                                                                      & ( n5 = F ) )
                                                                  & ~ ( ( n2 = F )
                                                                      & ( n5 = E ) )
                                                                  & ~ ( ( n3 = E )
                                                                      & ( n3 = F ) ) ) )),
                                                              ( ( ~ ( ( n0 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n0 = E )
                                                                    & ( n4 = F ) )
                                                                & ~ ( ( n0 = E )
                                                                    & ( n5 = F ) )
                                                                & ~ ( ( n0 = F )
                                                                    & ( n5 = E ) )
                                                                & ~ ( ( n1 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n1 = E )
                                                                    & ( n4 = F ) )
                                                                & ~ ( ( n1 = E )
                                                                    & ( n5 = F ) )
                                                                & ~ ( ( n1 = F )
                                                                    & ( n5 = E ) )
                                                                & ~ ( ( n2 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n2 = E )
                                                                    & ( n4 = F ) )
                                                                & ~ ( ( n2 = E )
                                                                    & ( n5 = F ) )
                                                                & ~ ( ( n2 = F )
                                                                    & ( n5 = E ) )
                                                                & ~ ( ( n3 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n3 = E )
                                                                    & ( n4 = F ) ) )
                                                            <=> ( ~ ( ( n0 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n0 = E )
                                                                    & ( n4 = F ) )
                                                                & ~ ( ( n0 = E )
                                                                    & ( n5 = F ) )
                                                                & ~ ( ( n0 = F )
                                                                    & ( n5 = E ) )
                                                                & ~ ( ( n1 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n1 = E )
                                                                    & ( n4 = F ) )
                                                                & ~ ( ( n1 = E )
                                                                    & ( n5 = F ) )
                                                                & ~ ( ( n1 = F )
                                                                    & ( n5 = E ) )
                                                                & ~ ( ( n2 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n2 = E )
                                                                    & ( n4 = F ) )
                                                                & ~ ( ( n2 = E )
                                                                    & ( n5 = F ) )
                                                                & ~ ( ( n2 = F )
                                                                    & ( n5 = E ) )
                                                                & ~ ( ( n3 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n3 = E )
                                                                    & ( n4 = F ) ) ) )),
                                                            rewrite(( ( ~ ( ( n0 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n0 = E )
                                                                    & ( n4 = F ) )
                                                                & ~ ( ( n0 = E )
                                                                    & ( n5 = F ) )
                                                                & ~ ( ( n0 = F )
                                                                    & ( n5 = E ) )
                                                                & ~ ( ( n1 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n1 = E )
                                                                    & ( n4 = F ) )
                                                                & ~ ( ( n1 = E )
                                                                    & ( n5 = F ) )
                                                                & ~ ( ( n1 = F )
                                                                    & ( n5 = E ) )
                                                                & ~ ( ( n2 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n2 = E )
                                                                    & ( n4 = F ) )
                                                                & ~ ( ( n2 = E )
                                                                    & ( n5 = F ) )
                                                                & ~ ( ( n2 = F )
                                                                    & ( n5 = E ) )
                                                                & ~ ( ( n3 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n3 = E )
                                                                    & ( n4 = F ) ) )
                                                            <=> ( ~ ( ( n0 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n0 = E )
                                                                    & ( n4 = F ) )
                                                                & ~ ( ( n0 = E )
                                                                    & ( n5 = F ) )
                                                                & ~ ( ( n0 = F )
                                                                    & ( n5 = E ) )
                                                                & ~ ( ( n1 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n1 = E )
                                                                    & ( n4 = F ) )
                                                                & ~ ( ( n1 = E )
                                                                    & ( n5 = F ) )
                                                                & ~ ( ( n1 = F )
                                                                    & ( n5 = E ) )
                                                                & ~ ( ( n2 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n2 = E )
                                                                    & ( n4 = F ) )
                                                                & ~ ( ( n2 = E )
                                                                    & ( n5 = F ) )
                                                                & ~ ( ( n2 = F )
                                                                    & ( n5 = E ) )
                                                                & ~ ( ( n3 = E )
                                                                    & ( n3 = F ) )
                                                                & ~ ( ( n3 = E )
                                                                    & ( n4 = F ) ) ) )),
                                                            ( ( ~ ( ( n0 = E )
                                                                  & ( n3 = F ) )
                                                              & ~ ( ( n0 = E )
                                                                  & ( n4 = F ) )
                                                              & ~ ( ( n0 = E )
                                                                  & ( n5 = F ) )
                                                              & ~ ( ( n0 = F )
                                                                  & ( n5 = E ) )
                                                              & ~ ( ( n1 = E )
                                                                  & ( n3 = F ) )
                                                              & ~ ( ( n1 = E )
                                                                  & ( n4 = F ) )
                                                              & ~ ( ( n1 = E )
                                                                  & ( n5 = F ) )
                                                              & ~ ( ( n1 = F )
                                                                  & ( n5 = E ) )
                                                              & ~ ( ( n2 = E )
                                                                  & ( n3 = F ) )
                                                              & ~ ( ( n2 = E )
                                                                  & ( n4 = F ) )
                                                              & ~ ( ( n2 = E )
                                                                  & ( n5 = F ) )
                                                              & ~ ( ( n2 = F )
                                                                  & ( n5 = E ) )
                                                              & ~ ( ( n3 = E )
                                                                  & ( n3 = F ) )
                                                              & ~ ( ( n3 = E )
                                                                  & ( n4 = F ) ) )
                                                          <=> ( ~ ( ( n0 = E )
                                                                  & ( n3 = F ) )
                                                              & ~ ( ( n0 = E )
                                                                  & ( n4 = F ) )
                                                              & ~ ( ( n0 = E )
                                                                  & ( n5 = F ) )
                                                              & ~ ( ( n0 = F )
                                                                  & ( n5 = E ) )
                                                              & ~ ( ( n1 = E )
                                                                  & ( n3 = F ) )
                                                              & ~ ( ( n1 = E )
                                                                  & ( n4 = F ) )
                                                              & ~ ( ( n1 = E )
                                                                  & ( n5 = F ) )
                                                              & ~ ( ( n1 = F )
                                                                  & ( n5 = E ) )
                                                              & ~ ( ( n2 = E )
                                                                  & ( n3 = F ) )
                                                              & ~ ( ( n2 = E )
                                                                  & ( n4 = F ) )
                                                              & ~ ( ( n2 = E )
                                                                  & ( n5 = F ) )
                                                              & ~ ( ( n2 = F )
                                                                  & ( n5 = E ) )
                                                              & ~ ( ( n3 = E )
                                                                  & ( n3 = F ) )
                                                              & ~ ( ( n3 = E )
                                                                  & ( n4 = F ) ) ) )),
                                                          ( ( ~ ( ( n0 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n0 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n0 = E )
                                                                & ( n5 = F ) )
                                                            & ~ ( ( n0 = F )
                                                                & ( n5 = E ) )
                                                            & ~ ( ( n1 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n1 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n1 = E )
                                                                & ( n5 = F ) )
                                                            & ~ ( ( n1 = F )
                                                                & ( n5 = E ) )
                                                            & ~ ( ( n2 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n2 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n2 = E )
                                                                & ( n5 = F ) )
                                                            & ~ ( ( n2 = F )
                                                                & ( n5 = E ) )
                                                            & ~ ( ( n3 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n3 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n3 = E )
                                                                & ( n5 = F ) ) )
                                                        <=> ( ~ ( ( n0 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n0 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n0 = E )
                                                                & ( n5 = F ) )
                                                            & ~ ( ( n0 = F )
                                                                & ( n5 = E ) )
                                                            & ~ ( ( n1 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n1 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n1 = E )
                                                                & ( n5 = F ) )
                                                            & ~ ( ( n1 = F )
                                                                & ( n5 = E ) )
                                                            & ~ ( ( n2 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n2 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n2 = E )
                                                                & ( n5 = F ) )
                                                            & ~ ( ( n2 = F )
                                                                & ( n5 = E ) )
                                                            & ~ ( ( n3 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n3 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n3 = E )
                                                                & ( n5 = F ) ) ) )),
                                                        rewrite(( ( ~ ( ( n0 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n0 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n0 = E )
                                                                & ( n5 = F ) )
                                                            & ~ ( ( n0 = F )
                                                                & ( n5 = E ) )
                                                            & ~ ( ( n1 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n1 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n1 = E )
                                                                & ( n5 = F ) )
                                                            & ~ ( ( n1 = F )
                                                                & ( n5 = E ) )
                                                            & ~ ( ( n2 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n2 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n2 = E )
                                                                & ( n5 = F ) )
                                                            & ~ ( ( n2 = F )
                                                                & ( n5 = E ) )
                                                            & ~ ( ( n3 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n3 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n3 = E )
                                                                & ( n5 = F ) ) )
                                                        <=> ( ~ ( ( n0 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n0 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n0 = E )
                                                                & ( n5 = F ) )
                                                            & ~ ( ( n0 = F )
                                                                & ( n5 = E ) )
                                                            & ~ ( ( n1 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n1 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n1 = E )
                                                                & ( n5 = F ) )
                                                            & ~ ( ( n1 = F )
                                                                & ( n5 = E ) )
                                                            & ~ ( ( n2 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n2 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n2 = E )
                                                                & ( n5 = F ) )
                                                            & ~ ( ( n2 = F )
                                                                & ( n5 = E ) )
                                                            & ~ ( ( n3 = E )
                                                                & ( n3 = F ) )
                                                            & ~ ( ( n3 = E )
                                                                & ( n4 = F ) )
                                                            & ~ ( ( n3 = E )
                                                                & ( n5 = F ) ) ) )),
                                                        ( ( ~ ( ( n0 = E )
                                                              & ( n3 = F ) )
                                                          & ~ ( ( n0 = E )
                                                              & ( n4 = F ) )
                                                          & ~ ( ( n0 = E )
                                                              & ( n5 = F ) )
                                                          & ~ ( ( n0 = F )
                                                              & ( n5 = E ) )
                                                          & ~ ( ( n1 = E )
                                                              & ( n3 = F ) )
                                                          & ~ ( ( n1 = E )
                                                              & ( n4 = F ) )
                                                          & ~ ( ( n1 = E )
                                                              & ( n5 = F ) )
                                                          & ~ ( ( n1 = F )
                                                              & ( n5 = E ) )
                                                          & ~ ( ( n2 = E )
                                                              & ( n3 = F ) )
                                                          & ~ ( ( n2 = E )
                                                              & ( n4 = F ) )
                                                          & ~ ( ( n2 = E )
                                                              & ( n5 = F ) )
                                                          & ~ ( ( n2 = F )
                                                              & ( n5 = E ) )
                                                          & ~ ( ( n3 = E )
                                                              & ( n3 = F ) )
                                                          & ~ ( ( n3 = E )
                                                              & ( n4 = F ) )
                                                          & ~ ( ( n3 = E )
                                                              & ( n5 = F ) ) )
                                                      <=> ( ~ ( ( n0 = E )
                                                              & ( n3 = F ) )
                                                          & ~ ( ( n0 = E )
                                                              & ( n4 = F ) )
                                                          & ~ ( ( n0 = E )
                                                              & ( n5 = F ) )
                                                          & ~ ( ( n0 = F )
                                                              & ( n5 = E ) )
                                                          & ~ ( ( n1 = E )
                                                              & ( n3 = F ) )
                                                          & ~ ( ( n1 = E )
                                                              & ( n4 = F ) )
                                                          & ~ ( ( n1 = E )
                                                              & ( n5 = F ) )
                                                          & ~ ( ( n1 = F )
                                                              & ( n5 = E ) )
                                                          & ~ ( ( n2 = E )
                                                              & ( n3 = F ) )
                                                          & ~ ( ( n2 = E )
                                                              & ( n4 = F ) )
                                                          & ~ ( ( n2 = E )
                                                              & ( n5 = F ) )
                                                          & ~ ( ( n2 = F )
                                                              & ( n5 = E ) )
                                                          & ~ ( ( n3 = E )
                                                              & ( n3 = F ) )
                                                          & ~ ( ( n3 = E )
                                                              & ( n4 = F ) )
                                                          & ~ ( ( n3 = E )
                                                              & ( n5 = F ) ) ) )),
                                                      ( ( ~ ( ( n0 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n0 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n0 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n0 = F )
                                                            & ( n5 = E ) )
                                                        & ~ ( ( n1 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n1 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n1 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n1 = F )
                                                            & ( n5 = E ) )
                                                        & ~ ( ( n2 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n2 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n2 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n2 = F )
                                                            & ( n5 = E ) )
                                                        & ~ ( ( n3 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n3 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n3 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n3 = F )
                                                            & ( n4 = E ) ) )
                                                    <=> ( ~ ( ( n0 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n0 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n0 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n0 = F )
                                                            & ( n5 = E ) )
                                                        & ~ ( ( n1 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n1 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n1 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n1 = F )
                                                            & ( n5 = E ) )
                                                        & ~ ( ( n2 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n2 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n2 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n2 = F )
                                                            & ( n5 = E ) )
                                                        & ~ ( ( n3 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n3 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n3 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n3 = F )
                                                            & ( n4 = E ) ) ) )),
                                                    rewrite(( ( ~ ( ( n0 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n0 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n0 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n0 = F )
                                                            & ( n5 = E ) )
                                                        & ~ ( ( n1 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n1 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n1 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n1 = F )
                                                            & ( n5 = E ) )
                                                        & ~ ( ( n2 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n2 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n2 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n2 = F )
                                                            & ( n5 = E ) )
                                                        & ~ ( ( n3 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n3 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n3 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n3 = F )
                                                            & ( n4 = E ) ) )
                                                    <=> ( ~ ( ( n0 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n0 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n0 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n0 = F )
                                                            & ( n5 = E ) )
                                                        & ~ ( ( n1 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n1 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n1 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n1 = F )
                                                            & ( n5 = E ) )
                                                        & ~ ( ( n2 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n2 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n2 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n2 = F )
                                                            & ( n5 = E ) )
                                                        & ~ ( ( n3 = E )
                                                            & ( n3 = F ) )
                                                        & ~ ( ( n3 = E )
                                                            & ( n4 = F ) )
                                                        & ~ ( ( n3 = E )
                                                            & ( n5 = F ) )
                                                        & ~ ( ( n3 = F )
                                                            & ( n4 = E ) ) ) )),
                                                    ( ( ~ ( ( n0 = E )
                                                          & ( n3 = F ) )
                                                      & ~ ( ( n0 = E )
                                                          & ( n4 = F ) )
                                                      & ~ ( ( n0 = E )
                                                          & ( n5 = F ) )
                                                      & ~ ( ( n0 = F )
                                                          & ( n5 = E ) )
                                                      & ~ ( ( n1 = E )
                                                          & ( n3 = F ) )
                                                      & ~ ( ( n1 = E )
                                                          & ( n4 = F ) )
                                                      & ~ ( ( n1 = E )
                                                          & ( n5 = F ) )
                                                      & ~ ( ( n1 = F )
                                                          & ( n5 = E ) )
                                                      & ~ ( ( n2 = E )
                                                          & ( n3 = F ) )
                                                      & ~ ( ( n2 = E )
                                                          & ( n4 = F ) )
                                                      & ~ ( ( n2 = E )
                                                          & ( n5 = F ) )
                                                      & ~ ( ( n2 = F )
                                                          & ( n5 = E ) )
                                                      & ~ ( ( n3 = E )
                                                          & ( n3 = F ) )
                                                      & ~ ( ( n3 = E )
                                                          & ( n4 = F ) )
                                                      & ~ ( ( n3 = E )
                                                          & ( n5 = F ) )
                                                      & ~ ( ( n3 = F )
                                                          & ( n4 = E ) ) )
                                                  <=> ( ~ ( ( n0 = E )
                                                          & ( n3 = F ) )
                                                      & ~ ( ( n0 = E )
                                                          & ( n4 = F ) )
                                                      & ~ ( ( n0 = E )
                                                          & ( n5 = F ) )
                                                      & ~ ( ( n0 = F )
                                                          & ( n5 = E ) )
                                                      & ~ ( ( n1 = E )
                                                          & ( n3 = F ) )
                                                      & ~ ( ( n1 = E )
                                                          & ( n4 = F ) )
                                                      & ~ ( ( n1 = E )
                                                          & ( n5 = F ) )
                                                      & ~ ( ( n1 = F )
                                                          & ( n5 = E ) )
                                                      & ~ ( ( n2 = E )
                                                          & ( n3 = F ) )
                                                      & ~ ( ( n2 = E )
                                                          & ( n4 = F ) )
                                                      & ~ ( ( n2 = E )
                                                          & ( n5 = F ) )
                                                      & ~ ( ( n2 = F )
                                                          & ( n5 = E ) )
                                                      & ~ ( ( n3 = E )
                                                          & ( n3 = F ) )
                                                      & ~ ( ( n3 = E )
                                                          & ( n4 = F ) )
                                                      & ~ ( ( n3 = E )
                                                          & ( n5 = F ) )
                                                      & ~ ( ( n3 = F )
                                                          & ( n4 = E ) ) ) )),
                                                  ( ( ~ ( ( n0 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n0 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n0 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n0 = F )
                                                        & ( n5 = E ) )
                                                    & ~ ( ( n1 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n1 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n1 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n1 = F )
                                                        & ( n5 = E ) )
                                                    & ~ ( ( n2 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n2 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n2 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n2 = F )
                                                        & ( n5 = E ) )
                                                    & ~ ( ( n3 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n3 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n3 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n3 = F )
                                                        & ( n4 = E ) )
                                                    & ~ ( ( n3 = F )
                                                        & ( n5 = E ) ) )
                                                <=> ( ~ ( ( n0 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n0 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n0 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n0 = F )
                                                        & ( n5 = E ) )
                                                    & ~ ( ( n1 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n1 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n1 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n1 = F )
                                                        & ( n5 = E ) )
                                                    & ~ ( ( n2 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n2 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n2 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n2 = F )
                                                        & ( n5 = E ) )
                                                    & ~ ( ( n3 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n3 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n3 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n3 = F )
                                                        & ( n4 = E ) )
                                                    & ~ ( ( n3 = F )
                                                        & ( n5 = E ) ) ) )),
                                                rewrite(( ( ~ ( ( n0 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n0 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n0 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n0 = F )
                                                        & ( n5 = E ) )
                                                    & ~ ( ( n1 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n1 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n1 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n1 = F )
                                                        & ( n5 = E ) )
                                                    & ~ ( ( n2 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n2 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n2 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n2 = F )
                                                        & ( n5 = E ) )
                                                    & ~ ( ( n3 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n3 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n3 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n3 = F )
                                                        & ( n4 = E ) )
                                                    & ~ ( ( n3 = F )
                                                        & ( n5 = E ) ) )
                                                <=> ( ~ ( ( n0 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n0 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n0 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n0 = F )
                                                        & ( n5 = E ) )
                                                    & ~ ( ( n1 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n1 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n1 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n1 = F )
                                                        & ( n5 = E ) )
                                                    & ~ ( ( n2 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n2 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n2 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n2 = F )
                                                        & ( n5 = E ) )
                                                    & ~ ( ( n3 = E )
                                                        & ( n3 = F ) )
                                                    & ~ ( ( n3 = E )
                                                        & ( n4 = F ) )
                                                    & ~ ( ( n3 = E )
                                                        & ( n5 = F ) )
                                                    & ~ ( ( n3 = F )
                                                        & ( n4 = E ) )
                                                    & ~ ( ( n3 = F )
                                                        & ( n5 = E ) ) ) )),
                                                ( ( ~ ( ( n0 = E )
                                                      & ( n3 = F ) )
                                                  & ~ ( ( n0 = E )
                                                      & ( n4 = F ) )
                                                  & ~ ( ( n0 = E )
                                                      & ( n5 = F ) )
                                                  & ~ ( ( n0 = F )
                                                      & ( n5 = E ) )
                                                  & ~ ( ( n1 = E )
                                                      & ( n3 = F ) )
                                                  & ~ ( ( n1 = E )
                                                      & ( n4 = F ) )
                                                  & ~ ( ( n1 = E )
                                                      & ( n5 = F ) )
                                                  & ~ ( ( n1 = F )
                                                      & ( n5 = E ) )
                                                  & ~ ( ( n2 = E )
                                                      & ( n3 = F ) )
                                                  & ~ ( ( n2 = E )
                                                      & ( n4 = F ) )
                                                  & ~ ( ( n2 = E )
                                                      & ( n5 = F ) )
                                                  & ~ ( ( n2 = F )
                                                      & ( n5 = E ) )
                                                  & ~ ( ( n3 = E )
                                                      & ( n3 = F ) )
                                                  & ~ ( ( n3 = E )
                                                      & ( n4 = F ) )
                                                  & ~ ( ( n3 = E )
                                                      & ( n5 = F ) )
                                                  & ~ ( ( n3 = F )
                                                      & ( n4 = E ) )
                                                  & ~ ( ( n3 = F )
                                                      & ( n5 = E ) ) )
                                              <=> ( ~ ( ( n0 = E )
                                                      & ( n3 = F ) )
                                                  & ~ ( ( n0 = E )
                                                      & ( n4 = F ) )
                                                  & ~ ( ( n0 = E )
                                                      & ( n5 = F ) )
                                                  & ~ ( ( n0 = F )
                                                      & ( n5 = E ) )
                                                  & ~ ( ( n1 = E )
                                                      & ( n3 = F ) )
                                                  & ~ ( ( n1 = E )
                                                      & ( n4 = F ) )
                                                  & ~ ( ( n1 = E )
                                                      & ( n5 = F ) )
                                                  & ~ ( ( n1 = F )
                                                      & ( n5 = E ) )
                                                  & ~ ( ( n2 = E )
                                                      & ( n3 = F ) )
                                                  & ~ ( ( n2 = E )
                                                      & ( n4 = F ) )
                                                  & ~ ( ( n2 = E )
                                                      & ( n5 = F ) )
                                                  & ~ ( ( n2 = F )
                                                      & ( n5 = E ) )
                                                  & ~ ( ( n3 = E )
                                                      & ( n3 = F ) )
                                                  & ~ ( ( n3 = E )
                                                      & ( n4 = F ) )
                                                  & ~ ( ( n3 = E )
                                                      & ( n5 = F ) )
                                                  & ~ ( ( n3 = F )
                                                      & ( n4 = E ) )
                                                  & ~ ( ( n3 = F )
                                                      & ( n5 = E ) ) ) )),
                                              ( ( ~ ( ( n0 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n0 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n0 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n0 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n1 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n1 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n1 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n1 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n2 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n2 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n2 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n2 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n3 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n3 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n3 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n3 = F )
                                                    & ( n4 = E ) )
                                                & ~ ( ( n3 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n4 = E )
                                                    & ( n4 = F ) ) )
                                            <=> ( ~ ( ( n0 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n0 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n0 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n0 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n1 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n1 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n1 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n1 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n2 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n2 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n2 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n2 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n3 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n3 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n3 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n3 = F )
                                                    & ( n4 = E ) )
                                                & ~ ( ( n3 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n4 = E )
                                                    & ( n4 = F ) ) ) )),
                                            rewrite(( ( ~ ( ( n0 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n0 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n0 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n0 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n1 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n1 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n1 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n1 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n2 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n2 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n2 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n2 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n3 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n3 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n3 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n3 = F )
                                                    & ( n4 = E ) )
                                                & ~ ( ( n3 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n4 = E )
                                                    & ( n4 = F ) ) )
                                            <=> ( ~ ( ( n0 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n0 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n0 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n0 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n1 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n1 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n1 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n1 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n2 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n2 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n2 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n2 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n3 = E )
                                                    & ( n3 = F ) )
                                                & ~ ( ( n3 = E )
                                                    & ( n4 = F ) )
                                                & ~ ( ( n3 = E )
                                                    & ( n5 = F ) )
                                                & ~ ( ( n3 = F )
                                                    & ( n4 = E ) )
                                                & ~ ( ( n3 = F )
                                                    & ( n5 = E ) )
                                                & ~ ( ( n4 = E )
                                                    & ( n4 = F ) ) ) )),
                                            ( ( ~ ( ( n0 = E )
                                                  & ( n3 = F ) )
                                              & ~ ( ( n0 = E )
                                                  & ( n4 = F ) )
                                              & ~ ( ( n0 = E )
                                                  & ( n5 = F ) )
                                              & ~ ( ( n0 = F )
                                                  & ( n5 = E ) )
                                              & ~ ( ( n1 = E )
                                                  & ( n3 = F ) )
                                              & ~ ( ( n1 = E )
                                                  & ( n4 = F ) )
                                              & ~ ( ( n1 = E )
                                                  & ( n5 = F ) )
                                              & ~ ( ( n1 = F )
                                                  & ( n5 = E ) )
                                              & ~ ( ( n2 = E )
                                                  & ( n3 = F ) )
                                              & ~ ( ( n2 = E )
                                                  & ( n4 = F ) )
                                              & ~ ( ( n2 = E )
                                                  & ( n5 = F ) )
                                              & ~ ( ( n2 = F )
                                                  & ( n5 = E ) )
                                              & ~ ( ( n3 = E )
                                                  & ( n3 = F ) )
                                              & ~ ( ( n3 = E )
                                                  & ( n4 = F ) )
                                              & ~ ( ( n3 = E )
                                                  & ( n5 = F ) )
                                              & ~ ( ( n3 = F )
                                                  & ( n4 = E ) )
                                              & ~ ( ( n3 = F )
                                                  & ( n5 = E ) )
                                              & ~ ( ( n4 = E )
                                                  & ( n4 = F ) ) )
                                          <=> ( ~ ( ( n0 = E )
                                                  & ( n3 = F ) )
                                              & ~ ( ( n0 = E )
                                                  & ( n4 = F ) )
                                              & ~ ( ( n0 = E )
                                                  & ( n5 = F ) )
                                              & ~ ( ( n0 = F )
                                                  & ( n5 = E ) )
                                              & ~ ( ( n1 = E )
                                                  & ( n3 = F ) )
                                              & ~ ( ( n1 = E )
                                                  & ( n4 = F ) )
                                              & ~ ( ( n1 = E )
                                                  & ( n5 = F ) )
                                              & ~ ( ( n1 = F )
                                                  & ( n5 = E ) )
                                              & ~ ( ( n2 = E )
                                                  & ( n3 = F ) )
                                              & ~ ( ( n2 = E )
                                                  & ( n4 = F ) )
                                              & ~ ( ( n2 = E )
                                                  & ( n5 = F ) )
                                              & ~ ( ( n2 = F )
                                                  & ( n5 = E ) )
                                              & ~ ( ( n3 = E )
                                                  & ( n3 = F ) )
                                              & ~ ( ( n3 = E )
                                                  & ( n4 = F ) )
                                              & ~ ( ( n3 = E )
                                                  & ( n5 = F ) )
                                              & ~ ( ( n3 = F )
                                                  & ( n4 = E ) )
                                              & ~ ( ( n3 = F )
                                                  & ( n5 = E ) )
                                              & ~ ( ( n4 = E )
                                                  & ( n4 = F ) ) ) )),
                                          ( ( ~ ( ( n0 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n0 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n0 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n0 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n1 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n1 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n1 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n1 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n2 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n2 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n2 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n2 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n3 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n3 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n3 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n3 = F )
                                                & ( n4 = E ) )
                                            & ~ ( ( n3 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n4 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n4 = E )
                                                & ( n5 = F ) ) )
                                        <=> ( ~ ( ( n0 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n0 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n0 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n0 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n1 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n1 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n1 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n1 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n2 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n2 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n2 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n2 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n3 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n3 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n3 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n3 = F )
                                                & ( n4 = E ) )
                                            & ~ ( ( n3 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n4 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n4 = E )
                                                & ( n5 = F ) ) ) )),
                                        rewrite(( ( ~ ( ( n0 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n0 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n0 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n0 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n1 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n1 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n1 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n1 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n2 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n2 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n2 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n2 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n3 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n3 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n3 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n3 = F )
                                                & ( n4 = E ) )
                                            & ~ ( ( n3 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n4 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n4 = E )
                                                & ( n5 = F ) ) )
                                        <=> ( ~ ( ( n0 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n0 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n0 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n0 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n1 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n1 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n1 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n1 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n2 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n2 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n2 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n2 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n3 = E )
                                                & ( n3 = F ) )
                                            & ~ ( ( n3 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n3 = E )
                                                & ( n5 = F ) )
                                            & ~ ( ( n3 = F )
                                                & ( n4 = E ) )
                                            & ~ ( ( n3 = F )
                                                & ( n5 = E ) )
                                            & ~ ( ( n4 = E )
                                                & ( n4 = F ) )
                                            & ~ ( ( n4 = E )
                                                & ( n5 = F ) ) ) )),
                                        ( ( ~ ( ( n0 = E )
                                              & ( n3 = F ) )
                                          & ~ ( ( n0 = E )
                                              & ( n4 = F ) )
                                          & ~ ( ( n0 = E )
                                              & ( n5 = F ) )
                                          & ~ ( ( n0 = F )
                                              & ( n5 = E ) )
                                          & ~ ( ( n1 = E )
                                              & ( n3 = F ) )
                                          & ~ ( ( n1 = E )
                                              & ( n4 = F ) )
                                          & ~ ( ( n1 = E )
                                              & ( n5 = F ) )
                                          & ~ ( ( n1 = F )
                                              & ( n5 = E ) )
                                          & ~ ( ( n2 = E )
                                              & ( n3 = F ) )
                                          & ~ ( ( n2 = E )
                                              & ( n4 = F ) )
                                          & ~ ( ( n2 = E )
                                              & ( n5 = F ) )
                                          & ~ ( ( n2 = F )
                                              & ( n5 = E ) )
                                          & ~ ( ( n3 = E )
                                              & ( n3 = F ) )
                                          & ~ ( ( n3 = E )
                                              & ( n4 = F ) )
                                          & ~ ( ( n3 = E )
                                              & ( n5 = F ) )
                                          & ~ ( ( n3 = F )
                                              & ( n4 = E ) )
                                          & ~ ( ( n3 = F )
                                              & ( n5 = E ) )
                                          & ~ ( ( n4 = E )
                                              & ( n4 = F ) )
                                          & ~ ( ( n4 = E )
                                              & ( n5 = F ) ) )
                                      <=> ( ~ ( ( n0 = E )
                                              & ( n3 = F ) )
                                          & ~ ( ( n0 = E )
                                              & ( n4 = F ) )
                                          & ~ ( ( n0 = E )
                                              & ( n5 = F ) )
                                          & ~ ( ( n0 = F )
                                              & ( n5 = E ) )
                                          & ~ ( ( n1 = E )
                                              & ( n3 = F ) )
                                          & ~ ( ( n1 = E )
                                              & ( n4 = F ) )
                                          & ~ ( ( n1 = E )
                                              & ( n5 = F ) )
                                          & ~ ( ( n1 = F )
                                              & ( n5 = E ) )
                                          & ~ ( ( n2 = E )
                                              & ( n3 = F ) )
                                          & ~ ( ( n2 = E )
                                              & ( n4 = F ) )
                                          & ~ ( ( n2 = E )
                                              & ( n5 = F ) )
                                          & ~ ( ( n2 = F )
                                              & ( n5 = E ) )
                                          & ~ ( ( n3 = E )
                                              & ( n3 = F ) )
                                          & ~ ( ( n3 = E )
                                              & ( n4 = F ) )
                                          & ~ ( ( n3 = E )
                                              & ( n5 = F ) )
                                          & ~ ( ( n3 = F )
                                              & ( n4 = E ) )
                                          & ~ ( ( n3 = F )
                                              & ( n5 = E ) )
                                          & ~ ( ( n4 = E )
                                              & ( n4 = F ) )
                                          & ~ ( ( n4 = E )
                                              & ( n5 = F ) ) ) )),
                                      ( ( ~ ( ( n0 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n0 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n0 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n0 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n1 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n1 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n1 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n1 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n2 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n2 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n2 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n2 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n3 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n3 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n3 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n3 = F )
                                            & ( n4 = E ) )
                                        & ~ ( ( n3 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n4 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n4 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n4 = F )
                                            & ( n5 = E ) ) )
                                    <=> ( ~ ( ( n0 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n0 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n0 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n0 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n1 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n1 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n1 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n1 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n2 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n2 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n2 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n2 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n3 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n3 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n3 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n3 = F )
                                            & ( n4 = E ) )
                                        & ~ ( ( n3 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n4 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n4 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n4 = F )
                                            & ( n5 = E ) ) ) )),
                                    rewrite(( ( ~ ( ( n0 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n0 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n0 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n0 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n1 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n1 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n1 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n1 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n2 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n2 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n2 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n2 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n3 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n3 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n3 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n3 = F )
                                            & ( n4 = E ) )
                                        & ~ ( ( n3 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n4 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n4 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n4 = F )
                                            & ( n5 = E ) ) )
                                    <=> ( ~ ( ( n0 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n0 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n0 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n0 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n1 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n1 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n1 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n1 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n2 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n2 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n2 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n2 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n3 = E )
                                            & ( n3 = F ) )
                                        & ~ ( ( n3 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n3 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n3 = F )
                                            & ( n4 = E ) )
                                        & ~ ( ( n3 = F )
                                            & ( n5 = E ) )
                                        & ~ ( ( n4 = E )
                                            & ( n4 = F ) )
                                        & ~ ( ( n4 = E )
                                            & ( n5 = F ) )
                                        & ~ ( ( n4 = F )
                                            & ( n5 = E ) ) ) )),
                                    ( ( ~ ( ( n0 = E )
                                          & ( n3 = F ) )
                                      & ~ ( ( n0 = E )
                                          & ( n4 = F ) )
                                      & ~ ( ( n0 = E )
                                          & ( n5 = F ) )
                                      & ~ ( ( n0 = F )
                                          & ( n5 = E ) )
                                      & ~ ( ( n1 = E )
                                          & ( n3 = F ) )
                                      & ~ ( ( n1 = E )
                                          & ( n4 = F ) )
                                      & ~ ( ( n1 = E )
                                          & ( n5 = F ) )
                                      & ~ ( ( n1 = F )
                                          & ( n5 = E ) )
                                      & ~ ( ( n2 = E )
                                          & ( n3 = F ) )
                                      & ~ ( ( n2 = E )
                                          & ( n4 = F ) )
                                      & ~ ( ( n2 = E )
                                          & ( n5 = F ) )
                                      & ~ ( ( n2 = F )
                                          & ( n5 = E ) )
                                      & ~ ( ( n3 = E )
                                          & ( n3 = F ) )
                                      & ~ ( ( n3 = E )
                                          & ( n4 = F ) )
                                      & ~ ( ( n3 = E )
                                          & ( n5 = F ) )
                                      & ~ ( ( n3 = F )
                                          & ( n4 = E ) )
                                      & ~ ( ( n3 = F )
                                          & ( n5 = E ) )
                                      & ~ ( ( n4 = E )
                                          & ( n4 = F ) )
                                      & ~ ( ( n4 = E )
                                          & ( n5 = F ) )
                                      & ~ ( ( n4 = F )
                                          & ( n5 = E ) ) )
                                  <=> ( ~ ( ( n0 = E )
                                          & ( n3 = F ) )
                                      & ~ ( ( n0 = E )
                                          & ( n4 = F ) )
                                      & ~ ( ( n0 = E )
                                          & ( n5 = F ) )
                                      & ~ ( ( n0 = F )
                                          & ( n5 = E ) )
                                      & ~ ( ( n1 = E )
                                          & ( n3 = F ) )
                                      & ~ ( ( n1 = E )
                                          & ( n4 = F ) )
                                      & ~ ( ( n1 = E )
                                          & ( n5 = F ) )
                                      & ~ ( ( n1 = F )
                                          & ( n5 = E ) )
                                      & ~ ( ( n2 = E )
                                          & ( n3 = F ) )
                                      & ~ ( ( n2 = E )
                                          & ( n4 = F ) )
                                      & ~ ( ( n2 = E )
                                          & ( n5 = F ) )
                                      & ~ ( ( n2 = F )
                                          & ( n5 = E ) )
                                      & ~ ( ( n3 = E )
                                          & ( n3 = F ) )
                                      & ~ ( ( n3 = E )
                                          & ( n4 = F ) )
                                      & ~ ( ( n3 = E )
                                          & ( n5 = F ) )
                                      & ~ ( ( n3 = F )
                                          & ( n4 = E ) )
                                      & ~ ( ( n3 = F )
                                          & ( n5 = E ) )
                                      & ~ ( ( n4 = E )
                                          & ( n4 = F ) )
                                      & ~ ( ( n4 = E )
                                          & ( n5 = F ) )
                                      & ~ ( ( n4 = F )
                                          & ( n5 = E ) ) ) )),
                                  ( ( ~ ( ( n0 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n0 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n0 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n0 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n1 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n1 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n1 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n1 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n2 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n2 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n2 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n2 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n3 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n3 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n3 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n3 = F )
                                        & ( n4 = E ) )
                                    & ~ ( ( n3 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n4 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n4 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n4 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n5 = E )
                                        & ( n5 = F ) ) )
                                <=> ( ~ ( ( n0 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n0 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n0 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n0 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n1 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n1 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n1 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n1 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n2 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n2 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n2 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n2 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n3 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n3 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n3 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n3 = F )
                                        & ( n4 = E ) )
                                    & ~ ( ( n3 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n4 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n4 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n4 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n5 = E )
                                        & ( n5 = F ) ) ) )),
                                rewrite(( ( ~ ( ( n0 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n0 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n0 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n0 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n1 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n1 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n1 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n1 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n2 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n2 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n2 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n2 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n3 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n3 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n3 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n3 = F )
                                        & ( n4 = E ) )
                                    & ~ ( ( n3 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n4 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n4 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n4 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n5 = E )
                                        & ( n5 = F ) ) )
                                <=> ( ~ ( ( n0 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n0 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n0 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n0 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n1 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n1 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n1 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n1 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n2 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n2 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n2 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n2 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n3 = E )
                                        & ( n3 = F ) )
                                    & ~ ( ( n3 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n3 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n3 = F )
                                        & ( n4 = E ) )
                                    & ~ ( ( n3 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n4 = E )
                                        & ( n4 = F ) )
                                    & ~ ( ( n4 = E )
                                        & ( n5 = F ) )
                                    & ~ ( ( n4 = F )
                                        & ( n5 = E ) )
                                    & ~ ( ( n5 = E )
                                        & ( n5 = F ) ) ) )),
                                ( ( ~ ( ( n0 = E )
                                      & ( n3 = F ) )
                                  & ~ ( ( n0 = E )
                                      & ( n4 = F ) )
                                  & ~ ( ( n0 = E )
                                      & ( n5 = F ) )
                                  & ~ ( ( n0 = F )
                                      & ( n5 = E ) )
                                  & ~ ( ( n1 = E )
                                      & ( n3 = F ) )
                                  & ~ ( ( n1 = E )
                                      & ( n4 = F ) )
                                  & ~ ( ( n1 = E )
                                      & ( n5 = F ) )
                                  & ~ ( ( n1 = F )
                                      & ( n5 = E ) )
                                  & ~ ( ( n2 = E )
                                      & ( n3 = F ) )
                                  & ~ ( ( n2 = E )
                                      & ( n4 = F ) )
                                  & ~ ( ( n2 = E )
                                      & ( n5 = F ) )
                                  & ~ ( ( n2 = F )
                                      & ( n5 = E ) )
                                  & ~ ( ( n3 = E )
                                      & ( n3 = F ) )
                                  & ~ ( ( n3 = E )
                                      & ( n4 = F ) )
                                  & ~ ( ( n3 = E )
                                      & ( n5 = F ) )
                                  & ~ ( ( n3 = F )
                                      & ( n4 = E ) )
                                  & ~ ( ( n3 = F )
                                      & ( n5 = E ) )
                                  & ~ ( ( n4 = E )
                                      & ( n4 = F ) )
                                  & ~ ( ( n4 = E )
                                      & ( n5 = F ) )
                                  & ~ ( ( n4 = F )
                                      & ( n5 = E ) )
                                  & ~ ( ( n5 = E )
                                      & ( n5 = F ) ) )
                              <=> ( ~ ( ( n0 = E )
                                      & ( n3 = F ) )
                                  & ~ ( ( n0 = E )
                                      & ( n4 = F ) )
                                  & ~ ( ( n0 = E )
                                      & ( n5 = F ) )
                                  & ~ ( ( n0 = F )
                                      & ( n5 = E ) )
                                  & ~ ( ( n1 = E )
                                      & ( n3 = F ) )
                                  & ~ ( ( n1 = E )
                                      & ( n4 = F ) )
                                  & ~ ( ( n1 = E )
                                      & ( n5 = F ) )
                                  & ~ ( ( n1 = F )
                                      & ( n5 = E ) )
                                  & ~ ( ( n2 = E )
                                      & ( n3 = F ) )
                                  & ~ ( ( n2 = E )
                                      & ( n4 = F ) )
                                  & ~ ( ( n2 = E )
                                      & ( n5 = F ) )
                                  & ~ ( ( n2 = F )
                                      & ( n5 = E ) )
                                  & ~ ( ( n3 = E )
                                      & ( n3 = F ) )
                                  & ~ ( ( n3 = E )
                                      & ( n4 = F ) )
                                  & ~ ( ( n3 = E )
                                      & ( n5 = F ) )
                                  & ~ ( ( n3 = F )
                                      & ( n4 = E ) )
                                  & ~ ( ( n3 = F )
                                      & ( n5 = E ) )
                                  & ~ ( ( n4 = E )
                                      & ( n4 = F ) )
                                  & ~ ( ( n4 = E )
                                      & ( n5 = F ) )
                                  & ~ ( ( n4 = F )
                                      & ( n5 = E ) )
                                  & ~ ( ( n5 = E )
                                      & ( n5 = F ) ) ) )),
                              ( ( ~ ( ( n0 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n0 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n0 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n0 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n1 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n1 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n1 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n1 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n2 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n2 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n2 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n2 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n3 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n3 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n3 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n3 = F )
                                    & ( n4 = E ) )
                                & ~ ( ( n3 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n4 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n4 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n4 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n5 = E )
                                    & ( n5 = F ) )
                                & ( n2 = F ) )
                            <=> ( ~ ( ( n0 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n0 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n0 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n0 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n1 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n1 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n1 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n1 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n2 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n2 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n2 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n2 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n3 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n3 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n3 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n3 = F )
                                    & ( n4 = E ) )
                                & ~ ( ( n3 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n4 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n4 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n4 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n5 = E )
                                    & ( n5 = F ) )
                                & ( n2 = F ) ) )),
                            rewrite(( ( ~ ( ( n0 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n0 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n0 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n0 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n1 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n1 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n1 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n1 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n2 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n2 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n2 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n2 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n3 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n3 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n3 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n3 = F )
                                    & ( n4 = E ) )
                                & ~ ( ( n3 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n4 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n4 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n4 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n5 = E )
                                    & ( n5 = F ) )
                                & ( n2 = F ) )
                            <=> ( ~ ( ( n0 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n0 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n0 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n0 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n1 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n1 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n1 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n1 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n2 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n2 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n2 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n2 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n3 = E )
                                    & ( n3 = F ) )
                                & ~ ( ( n3 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n3 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n3 = F )
                                    & ( n4 = E ) )
                                & ~ ( ( n3 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n4 = E )
                                    & ( n4 = F ) )
                                & ~ ( ( n4 = E )
                                    & ( n5 = F ) )
                                & ~ ( ( n4 = F )
                                    & ( n5 = E ) )
                                & ~ ( ( n5 = E )
                                    & ( n5 = F ) )
                                & ( n2 = F ) ) )),
                            ( ( ~ ( ( n0 = E )
                                  & ( n3 = F ) )
                              & ~ ( ( n0 = E )
                                  & ( n4 = F ) )
                              & ~ ( ( n0 = E )
                                  & ( n5 = F ) )
                              & ~ ( ( n0 = F )
                                  & ( n5 = E ) )
                              & ~ ( ( n1 = E )
                                  & ( n3 = F ) )
                              & ~ ( ( n1 = E )
                                  & ( n4 = F ) )
                              & ~ ( ( n1 = E )
                                  & ( n5 = F ) )
                              & ~ ( ( n1 = F )
                                  & ( n5 = E ) )
                              & ~ ( ( n2 = E )
                                  & ( n3 = F ) )
                              & ~ ( ( n2 = E )
                                  & ( n4 = F ) )
                              & ~ ( ( n2 = E )
                                  & ( n5 = F ) )
                              & ~ ( ( n2 = F )
                                  & ( n5 = E ) )
                              & ~ ( ( n3 = E )
                                  & ( n3 = F ) )
                              & ~ ( ( n3 = E )
                                  & ( n4 = F ) )
                              & ~ ( ( n3 = E )
                                  & ( n5 = F ) )
                              & ~ ( ( n3 = F )
                                  & ( n4 = E ) )
                              & ~ ( ( n3 = F )
                                  & ( n5 = E ) )
                              & ~ ( ( n4 = E )
                                  & ( n4 = F ) )
                              & ~ ( ( n4 = E )
                                  & ( n5 = F ) )
                              & ~ ( ( n4 = F )
                                  & ( n5 = E ) )
                              & ~ ( ( n5 = E )
                                  & ( n5 = F ) )
                              & ( n2 = F ) )
                          <=> ( ~ ( ( n0 = E )
                                  & ( n3 = F ) )
                              & ~ ( ( n0 = E )
                                  & ( n4 = F ) )
                              & ~ ( ( n0 = E )
                                  & ( n5 = F ) )
                              & ~ ( ( n0 = F )
                                  & ( n5 = E ) )
                              & ~ ( ( n1 = E )
                                  & ( n3 = F ) )
                              & ~ ( ( n1 = E )
                                  & ( n4 = F ) )
                              & ~ ( ( n1 = E )
                                  & ( n5 = F ) )
                              & ~ ( ( n1 = F )
                                  & ( n5 = E ) )
                              & ~ ( ( n2 = E )
                                  & ( n3 = F ) )
                              & ~ ( ( n2 = E )
                                  & ( n4 = F ) )
                              & ~ ( ( n2 = E )
                                  & ( n5 = F ) )
                              & ~ ( ( n2 = F )
                                  & ( n5 = E ) )
                              & ~ ( ( n3 = E )
                                  & ( n3 = F ) )
                              & ~ ( ( n3 = E )
                                  & ( n4 = F ) )
                              & ~ ( ( n3 = E )
                                  & ( n5 = F ) )
                              & ~ ( ( n3 = F )
                                  & ( n4 = E ) )
                              & ~ ( ( n3 = F )
                                  & ( n5 = E ) )
                              & ~ ( ( n4 = E )
                                  & ( n4 = F ) )
                              & ~ ( ( n4 = E )
                                  & ( n5 = F ) )
                              & ~ ( ( n4 = F )
                                  & ( n5 = E ) )
                              & ~ ( ( n5 = E )
                                  & ( n5 = F ) )
                              & ( n2 = F ) ) )),
                          ( ( ~ ( ( n0 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n0 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n0 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n0 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n1 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n1 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n1 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n1 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n2 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n2 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n2 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n2 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n3 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n3 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n3 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n3 = F )
                                & ( n4 = E ) )
                            & ~ ( ( n3 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n4 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n4 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n4 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n5 = E )
                                & ( n5 = F ) )
                            & ( n2 = F )
                            & ( n4 = E ) )
                        <=> ( ~ ( ( n0 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n0 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n0 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n0 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n1 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n1 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n1 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n1 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n2 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n2 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n2 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n2 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n3 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n3 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n3 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n3 = F )
                                & ( n4 = E ) )
                            & ~ ( ( n3 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n4 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n4 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n4 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n5 = E )
                                & ( n5 = F ) )
                            & ( n2 = F )
                            & ( n4 = E ) ) )),
                        rewrite(( ( ~ ( ( n0 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n0 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n0 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n0 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n1 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n1 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n1 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n1 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n2 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n2 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n2 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n2 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n3 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n3 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n3 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n3 = F )
                                & ( n4 = E ) )
                            & ~ ( ( n3 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n4 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n4 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n4 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n5 = E )
                                & ( n5 = F ) )
                            & ( n2 = F )
                            & ( n4 = E ) )
                        <=> ( ~ ( ( n0 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n0 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n0 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n0 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n1 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n1 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n1 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n1 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n2 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n2 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n2 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n2 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n3 = E )
                                & ( n3 = F ) )
                            & ~ ( ( n3 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n3 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n3 = F )
                                & ( n4 = E ) )
                            & ~ ( ( n3 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n4 = E )
                                & ( n4 = F ) )
                            & ~ ( ( n4 = E )
                                & ( n5 = F ) )
                            & ~ ( ( n4 = F )
                                & ( n5 = E ) )
                            & ~ ( ( n5 = E )
                                & ( n5 = F ) )
                            & ( n2 = F )
                            & ( n4 = E ) ) )),
                        ( ( ~ ( ( n0 = E )
                              & ( n3 = F ) )
                          & ~ ( ( n0 = E )
                              & ( n4 = F ) )
                          & ~ ( ( n0 = E )
                              & ( n5 = F ) )
                          & ~ ( ( n0 = F )
                              & ( n5 = E ) )
                          & ~ ( ( n1 = E )
                              & ( n3 = F ) )
                          & ~ ( ( n1 = E )
                              & ( n4 = F ) )
                          & ~ ( ( n1 = E )
                              & ( n5 = F ) )
                          & ~ ( ( n1 = F )
                              & ( n5 = E ) )
                          & ~ ( ( n2 = E )
                              & ( n3 = F ) )
                          & ~ ( ( n2 = E )
                              & ( n4 = F ) )
                          & ~ ( ( n2 = E )
                              & ( n5 = F ) )
                          & ~ ( ( n2 = F )
                              & ( n5 = E ) )
                          & ~ ( ( n3 = E )
                              & ( n3 = F ) )
                          & ~ ( ( n3 = E )
                              & ( n4 = F ) )
                          & ~ ( ( n3 = E )
                              & ( n5 = F ) )
                          & ~ ( ( n3 = F )
                              & ( n4 = E ) )
                          & ~ ( ( n3 = F )
                              & ( n5 = E ) )
                          & ~ ( ( n4 = E )
                              & ( n4 = F ) )
                          & ~ ( ( n4 = E )
                              & ( n5 = F ) )
                          & ~ ( ( n4 = F )
                              & ( n5 = E ) )
                          & ~ ( ( n5 = E )
                              & ( n5 = F ) )
                          & ( n2 = F )
                          & ( n4 = E ) )
                      <=> ( ~ ( ( n0 = E )
                              & ( n3 = F ) )
                          & ~ ( ( n0 = E )
                              & ( n4 = F ) )
                          & ~ ( ( n0 = E )
                              & ( n5 = F ) )
                          & ~ ( ( n0 = F )
                              & ( n5 = E ) )
                          & ~ ( ( n1 = E )
                              & ( n3 = F ) )
                          & ~ ( ( n1 = E )
                              & ( n4 = F ) )
                          & ~ ( ( n1 = E )
                              & ( n5 = F ) )
                          & ~ ( ( n1 = F )
                              & ( n5 = E ) )
                          & ~ ( ( n2 = E )
                              & ( n3 = F ) )
                          & ~ ( ( n2 = E )
                              & ( n4 = F ) )
                          & ~ ( ( n2 = E )
                              & ( n5 = F ) )
                          & ~ ( ( n2 = F )
                              & ( n5 = E ) )
                          & ~ ( ( n3 = E )
                              & ( n3 = F ) )
                          & ~ ( ( n3 = E )
                              & ( n4 = F ) )
                          & ~ ( ( n3 = E )
                              & ( n5 = F ) )
                          & ~ ( ( n3 = F )
                              & ( n4 = E ) )
                          & ~ ( ( n3 = F )
                              & ( n5 = E ) )
                          & ~ ( ( n4 = E )
                              & ( n4 = F ) )
                          & ~ ( ( n4 = E )
                              & ( n5 = F ) )
                          & ~ ( ( n4 = F )
                              & ( n5 = E ) )
                          & ~ ( ( n5 = E )
                              & ( n5 = F ) )
                          & ( n2 = F )
                          & ( n4 = E ) ) )),
                      ( ( ~ ( ( n0 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n0 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n0 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n0 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n1 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n1 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n1 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n1 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n2 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n2 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n2 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n2 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n3 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n3 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n3 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n3 = F )
                            & ( n4 = E ) )
                        & ~ ( ( n3 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n4 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n4 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n4 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n5 = E )
                            & ( n5 = F ) )
                        & ( n2 = F )
                        & ( n4 = E )
                        & ( n4 = F ) )
                    <=> ( ~ ( ( n0 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n0 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n0 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n0 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n1 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n1 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n1 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n1 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n2 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n2 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n2 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n2 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n3 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n3 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n3 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n3 = F )
                            & ( n4 = E ) )
                        & ~ ( ( n3 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n4 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n4 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n4 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n5 = E )
                            & ( n5 = F ) )
                        & ( n2 = F )
                        & ( n4 = E )
                        & ( n4 = F ) ) )),
                    rewrite(( ( ~ ( ( n0 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n0 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n0 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n0 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n1 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n1 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n1 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n1 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n2 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n2 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n2 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n2 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n3 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n3 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n3 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n3 = F )
                            & ( n4 = E ) )
                        & ~ ( ( n3 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n4 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n4 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n4 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n5 = E )
                            & ( n5 = F ) )
                        & ( n2 = F )
                        & ( n4 = E )
                        & ( n4 = F ) )
                    <=> ( ~ ( ( n0 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n0 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n0 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n0 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n1 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n1 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n1 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n1 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n2 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n2 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n2 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n2 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n3 = E )
                            & ( n3 = F ) )
                        & ~ ( ( n3 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n3 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n3 = F )
                            & ( n4 = E ) )
                        & ~ ( ( n3 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n4 = E )
                            & ( n4 = F ) )
                        & ~ ( ( n4 = E )
                            & ( n5 = F ) )
                        & ~ ( ( n4 = F )
                            & ( n5 = E ) )
                        & ~ ( ( n5 = E )
                            & ( n5 = F ) )
                        & ( n2 = F )
                        & ( n4 = E )
                        & ( n4 = F ) ) )),
                    ( ( ~ ( ( n0 = E )
                          & ( n3 = F ) )
                      & ~ ( ( n0 = E )
                          & ( n4 = F ) )
                      & ~ ( ( n0 = E )
                          & ( n5 = F ) )
                      & ~ ( ( n0 = F )
                          & ( n5 = E ) )
                      & ~ ( ( n1 = E )
                          & ( n3 = F ) )
                      & ~ ( ( n1 = E )
                          & ( n4 = F ) )
                      & ~ ( ( n1 = E )
                          & ( n5 = F ) )
                      & ~ ( ( n1 = F )
                          & ( n5 = E ) )
                      & ~ ( ( n2 = E )
                          & ( n3 = F ) )
                      & ~ ( ( n2 = E )
                          & ( n4 = F ) )
                      & ~ ( ( n2 = E )
                          & ( n5 = F ) )
                      & ~ ( ( n2 = F )
                          & ( n5 = E ) )
                      & ~ ( ( n3 = E )
                          & ( n3 = F ) )
                      & ~ ( ( n3 = E )
                          & ( n4 = F ) )
                      & ~ ( ( n3 = E )
                          & ( n5 = F ) )
                      & ~ ( ( n3 = F )
                          & ( n4 = E ) )
                      & ~ ( ( n3 = F )
                          & ( n5 = E ) )
                      & ~ ( ( n4 = E )
                          & ( n4 = F ) )
                      & ~ ( ( n4 = E )
                          & ( n5 = F ) )
                      & ~ ( ( n4 = F )
                          & ( n5 = E ) )
                      & ~ ( ( n5 = E )
                          & ( n5 = F ) )
                      & ( n2 = F )
                      & ( n4 = E )
                      & ( n4 = F ) )
                  <=> ( ~ ( ( n0 = E )
                          & ( n3 = F ) )
                      & ~ ( ( n0 = E )
                          & ( n4 = F ) )
                      & ~ ( ( n0 = E )
                          & ( n5 = F ) )
                      & ~ ( ( n0 = F )
                          & ( n5 = E ) )
                      & ~ ( ( n1 = E )
                          & ( n3 = F ) )
                      & ~ ( ( n1 = E )
                          & ( n4 = F ) )
                      & ~ ( ( n1 = E )
                          & ( n5 = F ) )
                      & ~ ( ( n1 = F )
                          & ( n5 = E ) )
                      & ~ ( ( n2 = E )
                          & ( n3 = F ) )
                      & ~ ( ( n2 = E )
                          & ( n4 = F ) )
                      & ~ ( ( n2 = E )
                          & ( n5 = F ) )
                      & ~ ( ( n2 = F )
                          & ( n5 = E ) )
                      & ~ ( ( n3 = E )
                          & ( n3 = F ) )
                      & ~ ( ( n3 = E )
                          & ( n4 = F ) )
                      & ~ ( ( n3 = E )
                          & ( n5 = F ) )
                      & ~ ( ( n3 = F )
                          & ( n4 = E ) )
                      & ~ ( ( n3 = F )
                          & ( n5 = E ) )
                      & ~ ( ( n4 = E )
                          & ( n4 = F ) )
                      & ~ ( ( n4 = E )
                          & ( n5 = F ) )
                      & ~ ( ( n4 = F )
                          & ( n5 = E ) )
                      & ~ ( ( n5 = E )
                          & ( n5 = F ) )
                      & ( n2 = F )
                      & ( n4 = E )
                      & ( n4 = F ) ) )),
                  ( ( ~ ( ( n0 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n0 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n0 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n0 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n1 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n1 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n1 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n1 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n2 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n2 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n2 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n2 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n3 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n3 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n3 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n3 = F )
                        & ( n4 = E ) )
                    & ~ ( ( n3 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n4 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n4 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n4 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n5 = E )
                        & ( n5 = F ) )
                    & ( n2 = F )
                    & ( n4 = E )
                    & ( n4 = F )
                    & ( n5 = E ) )
                <=> ( ~ ( ( n0 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n0 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n0 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n0 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n1 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n1 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n1 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n1 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n2 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n2 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n2 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n2 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n3 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n3 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n3 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n3 = F )
                        & ( n4 = E ) )
                    & ~ ( ( n3 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n4 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n4 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n4 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n5 = E )
                        & ( n5 = F ) )
                    & ( n2 = F )
                    & ( n4 = E )
                    & ( n4 = F )
                    & ( n5 = E ) ) )),
                rewrite(( ( ~ ( ( n0 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n0 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n0 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n0 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n1 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n1 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n1 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n1 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n2 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n2 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n2 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n2 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n3 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n3 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n3 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n3 = F )
                        & ( n4 = E ) )
                    & ~ ( ( n3 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n4 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n4 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n4 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n5 = E )
                        & ( n5 = F ) )
                    & ( n2 = F )
                    & ( n4 = E )
                    & ( n4 = F )
                    & ( n5 = E ) )
                <=> ( ~ ( ( n0 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n0 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n0 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n0 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n1 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n1 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n1 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n1 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n2 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n2 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n2 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n2 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n3 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n3 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n3 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n3 = F )
                        & ( n4 = E ) )
                    & ~ ( ( n3 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n4 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n4 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n4 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n5 = E )
                        & ( n5 = F ) )
                    & ( n2 = F )
                    & ( n4 = E )
                    & ( n4 = F )
                    & ( n5 = E ) ) )),
                ( ( ~ ( ( n0 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n0 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n1 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n1 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n2 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n2 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n3 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n3 = F )
                      & ( n4 = E ) )
                  & ~ ( ( n3 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n4 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n4 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n4 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n5 = E )
                      & ( n5 = F ) )
                  & ( n2 = F )
                  & ( n4 = E )
                  & ( n4 = F )
                  & ( n5 = E ) )
              <=> ( ~ ( ( n0 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n0 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n1 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n1 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n2 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n2 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n3 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n3 = F )
                      & ( n4 = E ) )
                  & ~ ( ( n3 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n4 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n4 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n4 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n5 = E )
                      & ( n5 = F ) )
                  & ( n2 = F )
                  & ( n4 = E )
                  & ( n4 = F )
                  & ( n5 = E ) ) )),
              ( ( ( ~ ( ( n0 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n0 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n1 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n1 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n2 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n2 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n3 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n3 = F )
                      & ( n4 = E ) )
                  & ~ ( ( n3 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n4 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n4 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n4 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n5 = E )
                      & ( n5 = F ) )
                  & ( n2 = F )
                  & ( n4 = E )
                  & ( n4 = F )
                  & ( n5 = E ) )
               => ( a_select2(xinit_noise,n4) = n0 ) )
            <=> ( ( ~ ( ( n0 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n0 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n1 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n1 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n2 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n2 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n3 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n3 = F )
                      & ( n4 = E ) )
                  & ~ ( ( n3 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n4 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n4 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n4 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n5 = E )
                      & ( n5 = F ) )
                  & ( n2 = F )
                  & ( n4 = E )
                  & ( n4 = F )
                  & ( n5 = E ) )
               => ( a_select2(xinit_noise,n4) = n0 ) ) )),
            rewrite(( ( ( ~ ( ( n0 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n0 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n1 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n1 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n2 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n2 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n3 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n3 = F )
                      & ( n4 = E ) )
                  & ~ ( ( n3 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n4 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n4 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n4 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n5 = E )
                      & ( n5 = F ) )
                  & ( n2 = F )
                  & ( n4 = E )
                  & ( n4 = F )
                  & ( n5 = E ) )
               => ( a_select2(xinit_noise,n4) = n0 ) )
            <=> ( ~ ( ~ ( ( n0 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n0 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n0 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n0 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n1 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n1 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n1 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n1 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n2 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n2 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n2 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n2 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n3 = E )
                        & ( n3 = F ) )
                    & ~ ( ( n3 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n3 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n3 = F )
                        & ( n4 = E ) )
                    & ~ ( ( n3 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n4 = E )
                        & ( n4 = F ) )
                    & ~ ( ( n4 = E )
                        & ( n5 = F ) )
                    & ~ ( ( n4 = F )
                        & ( n5 = E ) )
                    & ~ ( ( n5 = E )
                        & ( n5 = F ) )
                    & ( n2 = F )
                    & ( n4 = E )
                    & ( n4 = F )
                    & ( n5 = E ) )
                | ( a_select2(xinit_noise,n4) = n0 ) ) )),
            ( ( ( ~ ( ( n0 = E )
                    & ( n3 = F ) )
                & ~ ( ( n0 = E )
                    & ( n4 = F ) )
                & ~ ( ( n0 = E )
                    & ( n5 = F ) )
                & ~ ( ( n0 = F )
                    & ( n5 = E ) )
                & ~ ( ( n1 = E )
                    & ( n3 = F ) )
                & ~ ( ( n1 = E )
                    & ( n4 = F ) )
                & ~ ( ( n1 = E )
                    & ( n5 = F ) )
                & ~ ( ( n1 = F )
                    & ( n5 = E ) )
                & ~ ( ( n2 = E )
                    & ( n3 = F ) )
                & ~ ( ( n2 = E )
                    & ( n4 = F ) )
                & ~ ( ( n2 = E )
                    & ( n5 = F ) )
                & ~ ( ( n2 = F )
                    & ( n5 = E ) )
                & ~ ( ( n3 = E )
                    & ( n3 = F ) )
                & ~ ( ( n3 = E )
                    & ( n4 = F ) )
                & ~ ( ( n3 = E )
                    & ( n5 = F ) )
                & ~ ( ( n3 = F )
                    & ( n4 = E ) )
                & ~ ( ( n3 = F )
                    & ( n5 = E ) )
                & ~ ( ( n4 = E )
                    & ( n4 = F ) )
                & ~ ( ( n4 = E )
                    & ( n5 = F ) )
                & ~ ( ( n4 = F )
                    & ( n5 = E ) )
                & ~ ( ( n5 = E )
                    & ( n5 = F ) )
                & ( n2 = F )
                & ( n4 = E )
                & ( n4 = F )
                & ( n5 = E ) )
             => ( a_select2(xinit_noise,n4) = n0 ) )
          <=> ( ~ ( ~ ( ( n0 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n0 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n1 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n1 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n2 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n2 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n3 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n3 = F )
                      & ( n4 = E ) )
                  & ~ ( ( n3 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n4 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n4 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n4 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n5 = E )
                      & ( n5 = F ) )
                  & ( n2 = F )
                  & ( n4 = E )
                  & ( n4 = F )
                  & ( n5 = E ) )
              | ( a_select2(xinit_noise,n4) = n0 ) ) )),
          ( ( ( leq(n0,E)
              & leq(n0,F)
              & leq(E,n5)
              & leq(F,n5) )
           => ( ( ~ ( ( n0 = E )
                    & ( n3 = F ) )
                & ~ ( ( n0 = E )
                    & ( n4 = F ) )
                & ~ ( ( n0 = E )
                    & ( n5 = F ) )
                & ~ ( ( n0 = F )
                    & ( n5 = E ) )
                & ~ ( ( n1 = E )
                    & ( n3 = F ) )
                & ~ ( ( n1 = E )
                    & ( n4 = F ) )
                & ~ ( ( n1 = E )
                    & ( n5 = F ) )
                & ~ ( ( n1 = F )
                    & ( n5 = E ) )
                & ~ ( ( n2 = E )
                    & ( n3 = F ) )
                & ~ ( ( n2 = E )
                    & ( n4 = F ) )
                & ~ ( ( n2 = E )
                    & ( n5 = F ) )
                & ~ ( ( n2 = F )
                    & ( n5 = E ) )
                & ~ ( ( n3 = E )
                    & ( n3 = F ) )
                & ~ ( ( n3 = E )
                    & ( n4 = F ) )
                & ~ ( ( n3 = E )
                    & ( n5 = F ) )
                & ~ ( ( n3 = F )
                    & ( n4 = E ) )
                & ~ ( ( n3 = F )
                    & ( n5 = E ) )
                & ~ ( ( n4 = E )
                    & ( n4 = F ) )
                & ~ ( ( n4 = E )
                    & ( n5 = F ) )
                & ~ ( ( n4 = F )
                    & ( n5 = E ) )
                & ~ ( ( n5 = E )
                    & ( n5 = F ) )
                & ( n2 = F )
                & ( n4 = E )
                & ( n4 = F )
                & ( n5 = E ) )
             => ( a_select2(xinit_noise,n4) = n0 ) ) )
        <=> ( ( leq(n0,E)
              & leq(n0,F)
              & leq(E,n5)
              & leq(F,n5) )
           => ( ~ ( ~ ( ( n0 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n0 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n1 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n1 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n2 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n2 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n3 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n3 = F )
                      & ( n4 = E ) )
                  & ~ ( ( n3 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n4 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n4 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n4 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n5 = E )
                      & ( n5 = F ) )
                  & ( n2 = F )
                  & ( n4 = E )
                  & ( n4 = F )
                  & ( n5 = E ) )
              | ( a_select2(xinit_noise,n4) = n0 ) ) ) )),
        rewrite(( ( ( leq(n0,E)
              & leq(n0,F)
              & leq(E,n5)
              & leq(F,n5) )
           => ( ~ ( ~ ( ( n0 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n0 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n0 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n1 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n1 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n1 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n2 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n2 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n2 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n3 = E )
                      & ( n3 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n3 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n3 = F )
                      & ( n4 = E ) )
                  & ~ ( ( n3 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n4 = E )
                      & ( n4 = F ) )
                  & ~ ( ( n4 = E )
                      & ( n5 = F ) )
                  & ~ ( ( n4 = F )
                      & ( n5 = E ) )
                  & ~ ( ( n5 = E )
                      & ( n5 = F ) )
                  & ( n2 = F )
                  & ( n4 = E )
                  & ( n4 = F )
                  & ( n5 = E ) )
              | ( a_select2(xinit_noise,n4) = n0 ) ) )
        <=> ( ( a_select2(xinit_noise,n4) = n0 )
            | ~ ( leq(n0,E)
                & leq(n0,F)
                & leq(E,n5)
                & leq(F,n5) )
            | ~ ( ~ ( ( n0 = E )
                    & ( n3 = F ) )
                & ~ ( ( n0 = E )
                    & ( n4 = F ) )
                & ~ ( ( n0 = E )
                    & ( n5 = F ) )
                & ~ ( ( n0 = F )
                    & ( n5 = E ) )
                & ~ ( ( n1 = E )
                    & ( n3 = F ) )
                & ~ ( ( n1 = E )
                    & ( n4 = F ) )
                & ~ ( ( n1 = E )
                    & ( n5 = F ) )
                & ~ ( ( n1 = F )
                    & ( n5 = E ) )
                & ~ ( ( n2 = E )
                    & ( n3 = F ) )
                & ~ ( ( n2 = E )
                    & ( n4 = F ) )
                & ~ ( ( n2 = E )
                    & ( n5 = F ) )
                & ~ ( ( n2 = F )
                    & ( n5 = E ) )
                & ~ ( ( n3 = E )
                    & ( n3 = F ) )
                & ~ ( ( n3 = E )
                    & ( n4 = F ) )
                & ~ ( ( n3 = E )
                    & ( n5 = F ) )
                & ~ ( ( n3 = F )
                    & ( n4 = E ) )
                & ~ ( ( n3 = F )
                    & ( n5 = E ) )
                & ~ ( ( n4 = E )
                    & ( n4 = F ) )
                & ~ ( ( n4 = E )
                    & ( n5 = F ) )
                & ~ ( ( n4 = F )
                    & ( n5 = E ) )
                & ~ ( ( n5 = E )
                    & ( n5 = F ) )
                & ( n2 = F )
                & ( n4 = E )
                & ( n4 = F )
                & ( n5 = E ) ) ) )),
        ( ( ( leq(n0,E)
            & leq(n0,F)
            & leq(E,n5)
            & leq(F,n5) )
         => ( ( ~ ( ( n0 = E )
                  & ( n3 = F ) )
              & ~ ( ( n0 = E )
                  & ( n4 = F ) )
              & ~ ( ( n0 = E )
                  & ( n5 = F ) )
              & ~ ( ( n0 = F )
                  & ( n5 = E ) )
              & ~ ( ( n1 = E )
                  & ( n3 = F ) )
              & ~ ( ( n1 = E )
                  & ( n4 = F ) )
              & ~ ( ( n1 = E )
                  & ( n5 = F ) )
              & ~ ( ( n1 = F )
                  & ( n5 = E ) )
              & ~ ( ( n2 = E )
                  & ( n3 = F ) )
              & ~ ( ( n2 = E )
                  & ( n4 = F ) )
              & ~ ( ( n2 = E )
                  & ( n5 = F ) )
              & ~ ( ( n2 = F )
                  & ( n5 = E ) )
              & ~ ( ( n3 = E )
                  & ( n3 = F ) )
              & ~ ( ( n3 = E )
                  & ( n4 = F ) )
              & ~ ( ( n3 = E )
                  & ( n5 = F ) )
              & ~ ( ( n3 = F )
                  & ( n4 = E ) )
              & ~ ( ( n3 = F )
                  & ( n5 = E ) )
              & ~ ( ( n4 = E )
                  & ( n4 = F ) )
              & ~ ( ( n4 = E )
                  & ( n5 = F ) )
              & ~ ( ( n4 = F )
                  & ( n5 = E ) )
              & ~ ( ( n5 = E )
                  & ( n5 = F ) )
              & ( n2 = F )
              & ( n4 = E )
              & ( n4 = F )
              & ( n5 = E ) )
           => ( a_select2(xinit_noise,n4) = n0 ) ) )
      <=> ( ( a_select2(xinit_noise,n4) = n0 )
          | ~ ( leq(n0,E)
              & leq(n0,F)
              & leq(E,n5)
              & leq(F,n5) )
          | ~ ( ~ ( ( n0 = E )
                  & ( n3 = F ) )
              & ~ ( ( n0 = E )
                  & ( n4 = F ) )
              & ~ ( ( n0 = E )
                  & ( n5 = F ) )
              & ~ ( ( n0 = F )
                  & ( n5 = E ) )
              & ~ ( ( n1 = E )
                  & ( n3 = F ) )
              & ~ ( ( n1 = E )
                  & ( n4 = F ) )
              & ~ ( ( n1 = E )
                  & ( n5 = F ) )
              & ~ ( ( n1 = F )
                  & ( n5 = E ) )
              & ~ ( ( n2 = E )
                  & ( n3 = F ) )
              & ~ ( ( n2 = E )
                  & ( n4 = F ) )
              & ~ ( ( n2 = E )
                  & ( n5 = F ) )
              & ~ ( ( n2 = F )
                  & ( n5 = E ) )
              & ~ ( ( n3 = E )
                  & ( n3 = F ) )
              & ~ ( ( n3 = E )
                  & ( n4 = F ) )
              & ~ ( ( n3 = E )
                  & ( n5 = F ) )
              & ~ ( ( n3 = F )
                  & ( n4 = E ) )
              & ~ ( ( n3 = F )
                  & ( n5 = E ) )
              & ~ ( ( n4 = E )
                  & ( n4 = F ) )
              & ~ ( ( n4 = E )
                  & ( n5 = F ) )
              & ~ ( ( n4 = F )
                  & ( n5 = E ) )
              & ~ ( ( n5 = E )
                  & ( n5 = F ) )
              & ( n2 = F )
              & ( n4 = E )
              & ( n4 = F )
              & ( n5 = E ) ) ) )),
    inference(bind,[status(th)],[]) ).

tff(31,plain,
    ( ! [E: $i,F: $i] :
        ( ( leq(n0,E)
          & leq(n0,F)
          & leq(E,n5)
          & leq(F,n5) )
       => ( ( ~ ( ( n0 = E )
                & ( n3 = F ) )
            & ~ ( ( n0 = E )
                & ( n4 = F ) )
            & ~ ( ( n0 = E )
                & ( n5 = F ) )
            & ~ ( ( n0 = F )
                & ( n5 = E ) )
            & ~ ( ( n1 = E )
                & ( n3 = F ) )
            & ~ ( ( n1 = E )
                & ( n4 = F ) )
            & ~ ( ( n1 = E )
                & ( n5 = F ) )
            & ~ ( ( n1 = F )
                & ( n5 = E ) )
            & ~ ( ( n2 = E )
                & ( n3 = F ) )
            & ~ ( ( n2 = E )
                & ( n4 = F ) )
            & ~ ( ( n2 = E )
                & ( n5 = F ) )
            & ~ ( ( n2 = F )
                & ( n5 = E ) )
            & ~ ( ( n3 = E )
                & ( n3 = F ) )
            & ~ ( ( n3 = E )
                & ( n4 = F ) )
            & ~ ( ( n3 = E )
                & ( n5 = F ) )
            & ~ ( ( n3 = F )
                & ( n4 = E ) )
            & ~ ( ( n3 = F )
                & ( n5 = E ) )
            & ~ ( ( n4 = E )
                & ( n4 = F ) )
            & ~ ( ( n4 = E )
                & ( n5 = F ) )
            & ~ ( ( n4 = F )
                & ( n5 = E ) )
            & ~ ( ( n5 = E )
                & ( n5 = F ) )
            & ( n2 = F )
            & ( n4 = E )
            & ( n4 = F )
            & ( n5 = E ) )
         => ( a_select2(xinit_noise,n4) = n0 ) ) )
  <=> ! [E: $i,F: $i] :
        ( ( a_select2(xinit_noise,n4) = n0 )
        | ~ ( leq(n0,E)
            & leq(n0,F)
            & leq(E,n5)
            & leq(F,n5) )
        | ~ ( ~ ( ( n0 = E )
                & ( n3 = F ) )
            & ~ ( ( n0 = E )
                & ( n4 = F ) )
            & ~ ( ( n0 = E )
                & ( n5 = F ) )
            & ~ ( ( n0 = F )
                & ( n5 = E ) )
            & ~ ( ( n1 = E )
                & ( n3 = F ) )
            & ~ ( ( n1 = E )
                & ( n4 = F ) )
            & ~ ( ( n1 = E )
                & ( n5 = F ) )
            & ~ ( ( n1 = F )
                & ( n5 = E ) )
            & ~ ( ( n2 = E )
                & ( n3 = F ) )
            & ~ ( ( n2 = E )
                & ( n4 = F ) )
            & ~ ( ( n2 = E )
                & ( n5 = F ) )
            & ~ ( ( n2 = F )
                & ( n5 = E ) )
            & ~ ( ( n3 = E )
                & ( n3 = F ) )
            & ~ ( ( n3 = E )
                & ( n4 = F ) )
            & ~ ( ( n3 = E )
                & ( n5 = F ) )
            & ~ ( ( n3 = F )
                & ( n4 = E ) )
            & ~ ( ( n3 = F )
                & ( n5 = E ) )
            & ~ ( ( n4 = E )
                & ( n4 = F ) )
            & ~ ( ( n4 = E )
                & ( n5 = F ) )
            & ~ ( ( n4 = F )
                & ( n5 = E ) )
            & ~ ( ( n5 = E )
                & ( n5 = F ) )
            & ( n2 = F )
            & ( n4 = E )
            & ( n4 = F )
            & ( n5 = E ) ) ) ),
    inference(quant_intro,[status(thm)],[30]) ).

tff(32,plain,
    ( ! [E: $i,F: $i] :
        ( ( leq(n0,E)
          & leq(n0,F)
          & leq(E,n5)
          & leq(F,n5) )
       => ( ( ~ ( ( n0 = E )
                & ( n3 = F ) )
            & ~ ( ( n0 = E )
                & ( n4 = F ) )
            & ~ ( ( n0 = E )
                & ( n5 = F ) )
            & ~ ( ( n0 = F )
                & ( n5 = E ) )
            & ~ ( ( n1 = E )
                & ( n3 = F ) )
            & ~ ( ( n1 = E )
                & ( n4 = F ) )
            & ~ ( ( n1 = E )
                & ( n5 = F ) )
            & ~ ( ( n1 = F )
                & ( n5 = E ) )
            & ~ ( ( n2 = E )
                & ( n3 = F ) )
            & ~ ( ( n2 = E )
                & ( n4 = F ) )
            & ~ ( ( n2 = E )
                & ( n5 = F ) )
            & ~ ( ( n2 = F )
                & ( n5 = E ) )
            & ~ ( ( n3 = E )
                & ( n3 = F ) )
            & ~ ( ( n3 = E )
                & ( n4 = F ) )
            & ~ ( ( n3 = E )
                & ( n5 = F ) )
            & ~ ( ( n3 = F )
                & ( n4 = E ) )
            & ~ ( ( n3 = F )
                & ( n5 = E ) )
            & ~ ( ( n4 = E )
                & ( n4 = F ) )
            & ~ ( ( n4 = E )
                & ( n5 = F ) )
            & ~ ( ( n4 = F )
                & ( n5 = E ) )
            & ~ ( ( n5 = E )
                & ( n5 = F ) )
            & ( n2 = F )
            & ( n4 = E )
            & ( n4 = F )
            & ( n5 = E ) )
         => ( a_select2(xinit_noise,n4) = n0 ) ) )
  <=> $true ),
    inference(transitivity,[status(thm)],[31,29]) ).

tff(33,plain,
    ( ( ! [A: $i,B: $i] :
          ( ( leq(n0,A)
            & leq(n0,B)
            & leq(A,n5)
            & leq(B,n5) )
         => ( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ) )
      & ! [C: $i,D: $i] :
          ( ( leq(n0,C)
            & leq(n0,D)
            & leq(C,n2)
            & leq(D,n2) )
         => ( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ) ) )
  <=> ( ! [A: $i,B: $i] :
          ( ~ ( leq(n0,A)
              & leq(n0,B)
              & leq(A,n5)
              & leq(B,n5) )
          | ( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ) )
      & ! [C: $i,D: $i] :
          ( ~ ( leq(n0,C)
              & leq(n0,D)
              & leq(C,n2)
              & leq(D,n2) )
          | ( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ) ) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(34,plain,
    ( ( ( ! [A: $i,B: $i] :
            ( ( leq(n0,A)
              & leq(n0,B)
              & leq(A,n5)
              & leq(B,n5) )
           => ( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ) )
        & ! [C: $i,D: $i] :
            ( ( leq(n0,C)
              & leq(n0,D)
              & leq(C,n2)
              & leq(D,n2) )
           => ( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ) ) )
     => ! [E: $i,F: $i] :
          ( ( leq(n0,E)
            & leq(n0,F)
            & leq(E,n5)
            & leq(F,n5) )
         => ( ( ~ ( ( n0 = E )
                  & ( n3 = F ) )
              & ~ ( ( n0 = E )
                  & ( n4 = F ) )
              & ~ ( ( n0 = E )
                  & ( n5 = F ) )
              & ~ ( ( n0 = F )
                  & ( n5 = E ) )
              & ~ ( ( n1 = E )
                  & ( n3 = F ) )
              & ~ ( ( n1 = E )
                  & ( n4 = F ) )
              & ~ ( ( n1 = E )
                  & ( n5 = F ) )
              & ~ ( ( n1 = F )
                  & ( n5 = E ) )
              & ~ ( ( n2 = E )
                  & ( n3 = F ) )
              & ~ ( ( n2 = E )
                  & ( n4 = F ) )
              & ~ ( ( n2 = E )
                  & ( n5 = F ) )
              & ~ ( ( n2 = F )
                  & ( n5 = E ) )
              & ~ ( ( n3 = E )
                  & ( n3 = F ) )
              & ~ ( ( n3 = E )
                  & ( n4 = F ) )
              & ~ ( ( n3 = E )
                  & ( n5 = F ) )
              & ~ ( ( n3 = F )
                  & ( n4 = E ) )
              & ~ ( ( n3 = F )
                  & ( n5 = E ) )
              & ~ ( ( n4 = E )
                  & ( n4 = F ) )
              & ~ ( ( n4 = E )
                  & ( n5 = F ) )
              & ~ ( ( n4 = F )
                  & ( n5 = E ) )
              & ~ ( ( n5 = E )
                  & ( n5 = F ) )
              & ( n2 = F )
              & ( n4 = E )
              & ( n4 = F )
              & ( n5 = E ) )
           => ( a_select2(xinit_noise,n4) = n0 ) ) ) )
  <=> ( ( ! [A: $i,B: $i] :
            ( ~ ( leq(n0,A)
                & leq(n0,B)
                & leq(A,n5)
                & leq(B,n5) )
            | ( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ) )
        & ! [C: $i,D: $i] :
            ( ~ ( leq(n0,C)
                & leq(n0,D)
                & leq(C,n2)
                & leq(D,n2) )
            | ( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ) ) )
     => $true ) ),
    inference(monotonicity,[status(thm)],[33,32]) ).

tff(35,plain,
    ( ( ( ! [A: $i,B: $i] :
            ( ( leq(n0,A)
              & leq(n0,B)
              & leq(A,n5)
              & leq(B,n5) )
           => ( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ) )
        & ! [C: $i,D: $i] :
            ( ( leq(n0,C)
              & leq(n0,D)
              & leq(C,n2)
              & leq(D,n2) )
           => ( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ) ) )
     => ! [E: $i,F: $i] :
          ( ( leq(n0,E)
            & leq(n0,F)
            & leq(E,n5)
            & leq(F,n5) )
         => ( ( ~ ( ( n0 = E )
                  & ( n3 = F ) )
              & ~ ( ( n0 = E )
                  & ( n4 = F ) )
              & ~ ( ( n0 = E )
                  & ( n5 = F ) )
              & ~ ( ( n0 = F )
                  & ( n5 = E ) )
              & ~ ( ( n1 = E )
                  & ( n3 = F ) )
              & ~ ( ( n1 = E )
                  & ( n4 = F ) )
              & ~ ( ( n1 = E )
                  & ( n5 = F ) )
              & ~ ( ( n1 = F )
                  & ( n5 = E ) )
              & ~ ( ( n2 = E )
                  & ( n3 = F ) )
              & ~ ( ( n2 = E )
                  & ( n4 = F ) )
              & ~ ( ( n2 = E )
                  & ( n5 = F ) )
              & ~ ( ( n2 = F )
                  & ( n5 = E ) )
              & ~ ( ( n3 = E )
                  & ( n3 = F ) )
              & ~ ( ( n3 = E )
                  & ( n4 = F ) )
              & ~ ( ( n3 = E )
                  & ( n5 = F ) )
              & ~ ( ( n3 = F )
                  & ( n4 = E ) )
              & ~ ( ( n3 = F )
                  & ( n5 = E ) )
              & ~ ( ( n4 = E )
                  & ( n4 = F ) )
              & ~ ( ( n4 = E )
                  & ( n5 = F ) )
              & ~ ( ( n4 = F )
                  & ( n5 = E ) )
              & ~ ( ( n5 = E )
                  & ( n5 = F ) )
              & ( n2 = F )
              & ( n4 = E )
              & ( n4 = F )
              & ( n5 = E ) )
           => ( a_select2(xinit_noise,n4) = n0 ) ) ) )
  <=> $true ),
    inference(transitivity,[status(thm)],[34,2]) ).

tff(36,plain,
    ( ~ ( ( ! [A: $i,B: $i] :
              ( ( leq(n0,A)
                & leq(n0,B)
                & leq(A,n5)
                & leq(B,n5) )
             => ( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ) )
          & ! [C: $i,D: $i] :
              ( ( leq(n0,C)
                & leq(n0,D)
                & leq(C,n2)
                & leq(D,n2) )
             => ( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ) ) )
       => ! [E: $i,F: $i] :
            ( ( leq(n0,E)
              & leq(n0,F)
              & leq(E,n5)
              & leq(F,n5) )
           => ( ( ~ ( ( n0 = E )
                    & ( n3 = F ) )
                & ~ ( ( n0 = E )
                    & ( n4 = F ) )
                & ~ ( ( n0 = E )
                    & ( n5 = F ) )
                & ~ ( ( n0 = F )
                    & ( n5 = E ) )
                & ~ ( ( n1 = E )
                    & ( n3 = F ) )
                & ~ ( ( n1 = E )
                    & ( n4 = F ) )
                & ~ ( ( n1 = E )
                    & ( n5 = F ) )
                & ~ ( ( n1 = F )
                    & ( n5 = E ) )
                & ~ ( ( n2 = E )
                    & ( n3 = F ) )
                & ~ ( ( n2 = E )
                    & ( n4 = F ) )
                & ~ ( ( n2 = E )
                    & ( n5 = F ) )
                & ~ ( ( n2 = F )
                    & ( n5 = E ) )
                & ~ ( ( n3 = E )
                    & ( n3 = F ) )
                & ~ ( ( n3 = E )
                    & ( n4 = F ) )
                & ~ ( ( n3 = E )
                    & ( n5 = F ) )
                & ~ ( ( n3 = F )
                    & ( n4 = E ) )
                & ~ ( ( n3 = F )
                    & ( n5 = E ) )
                & ~ ( ( n4 = E )
                    & ( n4 = F ) )
                & ~ ( ( n4 = E )
                    & ( n5 = F ) )
                & ~ ( ( n4 = F )
                    & ( n5 = E ) )
                & ~ ( ( n5 = E )
                    & ( n5 = F ) )
                & ( n2 = F )
                & ( n4 = E )
                & ( n4 = F )
                & ( n5 = E ) )
             => ( a_select2(xinit_noise,n4) = n0 ) ) ) )
  <=> ~ $true ),
    inference(monotonicity,[status(thm)],[35]) ).

tff(37,plain,
    ( ~ ( ( ! [A: $i,B: $i] :
              ( ( leq(n0,A)
                & leq(n0,B)
                & leq(A,n5)
                & leq(B,n5) )
             => ( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ) )
          & ! [C: $i,D: $i] :
              ( ( leq(n0,C)
                & leq(n0,D)
                & leq(C,n2)
                & leq(D,n2) )
             => ( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ) ) )
       => ! [E: $i,F: $i] :
            ( ( leq(n0,E)
              & leq(n0,F)
              & leq(E,n5)
              & leq(F,n5) )
           => ( ( ~ ( ( n0 = E )
                    & ( n3 = F ) )
                & ~ ( ( n0 = E )
                    & ( n4 = F ) )
                & ~ ( ( n0 = E )
                    & ( n5 = F ) )
                & ~ ( ( n0 = F )
                    & ( n5 = E ) )
                & ~ ( ( n1 = E )
                    & ( n3 = F ) )
                & ~ ( ( n1 = E )
                    & ( n4 = F ) )
                & ~ ( ( n1 = E )
                    & ( n5 = F ) )
                & ~ ( ( n1 = F )
                    & ( n5 = E ) )
                & ~ ( ( n2 = E )
                    & ( n3 = F ) )
                & ~ ( ( n2 = E )
                    & ( n4 = F ) )
                & ~ ( ( n2 = E )
                    & ( n5 = F ) )
                & ~ ( ( n2 = F )
                    & ( n5 = E ) )
                & ~ ( ( n3 = E )
                    & ( n3 = F ) )
                & ~ ( ( n3 = E )
                    & ( n4 = F ) )
                & ~ ( ( n3 = E )
                    & ( n5 = F ) )
                & ~ ( ( n3 = F )
                    & ( n4 = E ) )
                & ~ ( ( n3 = F )
                    & ( n5 = E ) )
                & ~ ( ( n4 = E )
                    & ( n4 = F ) )
                & ~ ( ( n4 = E )
                    & ( n5 = F ) )
                & ~ ( ( n4 = F )
                    & ( n5 = E ) )
                & ~ ( ( n5 = E )
                    & ( n5 = F ) )
                & ( n2 = F )
                & ( n4 = E )
                & ( n4 = F )
                & ( n5 = E ) )
             => ( a_select2(xinit_noise,n4) = n0 ) ) ) )
  <=> $false ),
    inference(transitivity,[status(thm)],[36,1]) ).

tff(38,axiom,
    ~ ( ( ! [A: $i,B: $i] :
            ( ( leq(n0,A)
              & leq(n0,B)
              & leq(A,n5)
              & leq(B,n5) )
           => ( a_select3(q_ds1_filter,A,B) = a_select3(q_ds1_filter,B,A) ) )
        & ! [C: $i,D: $i] :
            ( ( leq(n0,C)
              & leq(n0,D)
              & leq(C,n2)
              & leq(D,n2) )
           => ( a_select3(r_ds1_filter,C,D) = a_select3(r_ds1_filter,D,C) ) ) )
     => ! [E: $i,F: $i] :
          ( ( leq(n0,E)
            & leq(n0,F)
            & leq(E,n5)
            & leq(F,n5) )
         => ( ( ~ ( ( n0 = E )
                  & ( n3 = F ) )
              & ~ ( ( n0 = E )
                  & ( n4 = F ) )
              & ~ ( ( n0 = E )
                  & ( n5 = F ) )
              & ~ ( ( n0 = F )
                  & ( n5 = E ) )
              & ~ ( ( n1 = E )
                  & ( n3 = F ) )
              & ~ ( ( n1 = E )
                  & ( n4 = F ) )
              & ~ ( ( n1 = E )
                  & ( n5 = F ) )
              & ~ ( ( n1 = F )
                  & ( n5 = E ) )
              & ~ ( ( n2 = E )
                  & ( n3 = F ) )
              & ~ ( ( n2 = E )
                  & ( n4 = F ) )
              & ~ ( ( n2 = E )
                  & ( n5 = F ) )
              & ~ ( ( n2 = F )
                  & ( n5 = E ) )
              & ~ ( ( n3 = E )
                  & ( n3 = F ) )
              & ~ ( ( n3 = E )
                  & ( n4 = F ) )
              & ~ ( ( n3 = E )
                  & ( n5 = F ) )
              & ~ ( ( n3 = F )
                  & ( n4 = E ) )
              & ~ ( ( n3 = F )
                  & ( n5 = E ) )
              & ~ ( ( n4 = E )
                  & ( n4 = F ) )
              & ~ ( ( n4 = E )
                  & ( n5 = F ) )
              & ~ ( ( n4 = F )
                  & ( n5 = E ) )
              & ~ ( ( n5 = E )
                  & ( n5 = F ) )
              & ( n2 = F )
              & ( n4 = E )
              & ( n4 = F )
              & ( n5 = E ) )
           => ( a_select2(xinit_noise,n4) = n0 ) ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quaternion_ds1_symm_0641) ).

tff(39,plain,
    $false,
    inference(modus_ponens,[status(thm)],[38,37]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem    : SWV227+1 : TPTP v9.0.0. Bugfixed v3.3.0.
% 0.03/0.12  % Command    : run_E %s %d THM
% 0.12/0.33  % Computer : n010.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit   : 300
% 0.12/0.33  % WCLimit    : 300
% 0.12/0.33  % DateTime   : Fri Jun 20 09:33:42 EDT 2025
% 0.12/0.33  % CPUTime    : 
% 0.20/0.38  % SZS status Theorem
% 0.20/0.38  % SZS output start Proof
% See solution above
% 0.20/0.47  % E exiting
%------------------------------------------------------------------------------