Leo-III---1.8.0.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : ALG194+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39

% Computer : n007.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Sun Sep 27 06:46:16 AM UTC 2026

% Result   : Theorem 20.25s 8.20s
% Output   : Refutation 20.74s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    3
%            Number of leaves      :    6
% Syntax   : Number of formulae    :   14 (   1 unt;   0 typ;   0 def)
%            Number of atoms       : 2871 (2870 equ;   0 cnn)
%            Maximal formula atoms :  686 ( 205 avg)
%            Number of connectives : 10755 ( 674   ~;1806   |;1051   &;7224   @)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :  295 (  78 avg)
%            Number of types       :    1 (   0 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :   10 (   8 usr;   8 con; 0-2 aty)
%            Number of variables   :    0 (   0   ^;   0   !;   0   ?;   0   :)

% Comments : 
%------------------------------------------------------------------------------
thf(op_decl,type,
    op: $i > $i > $i ).

thf(e0_decl,type,
    e0: $i ).

thf(e1_decl,type,
    e1: $i ).

thf(e2_decl,type,
    e2: $i ).

thf(e3_decl,type,
    e3: $i ).

thf(e4_decl,type,
    e4: $i ).

thf(e5_decl,type,
    e5: $i ).

thf(e6_decl,type,
    e6: $i ).

thf(6,axiom,
    ( ( ( e5 @ ( e6 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e6 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e6 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e6 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e6 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e6 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e6 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e6 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e6 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e6 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e6 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e6 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e6 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e6 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e6 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e6 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e6 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e6 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e6 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e6 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e6 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e5 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e5 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e5 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e5 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e5 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e5 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e5 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e5 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e4 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e4 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e3 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e3 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e3 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e2 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e3 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e2 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e1 @ ( e3 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e3 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e3 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e2 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e3 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e2 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e1 @ ( e2 @ op ) ) )
    & ( ( e5 @ ( e1 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e3 @ ( e1 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e3 @ ( e1 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e2 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e3 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e2 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e1 @ ( e1 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e6 @ ( e0 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e6 @ ( e0 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e6 @ ( e0 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e4 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e6 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e4 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e3 @ ( e0 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e6 @ ( e0 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e4 @ ( e0 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e3 @ ( e0 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e2 @ ( e0 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e6 @ ( e0 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e4 @ ( e0 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e3 @ ( e0 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e2 @ ( e0 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e1 @ ( e0 @ op ) ) )
    & ( ( e6 @ ( e5 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e6 @ ( e4 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e6 @ ( e4 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e6 @ ( e3 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e6 @ ( e3 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e6 @ ( e3 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e6 @ ( e2 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e6 @ ( e2 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e6 @ ( e2 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e6 @ ( e2 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e6 @ ( e1 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e6 @ ( e1 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e6 @ ( e1 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e6 @ ( e1 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e6 @ ( e1 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e6 @ ( e0 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e6 @ ( e0 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e6 @ ( e0 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e6 @ ( e0 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e6 @ ( e0 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e6 @ ( e0 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e5 @ ( e5 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e4 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e4 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e3 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e3 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e3 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e5 @ ( e1 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e1 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e1 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e1 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e5 @ ( e1 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e4 @ ( e5 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e4 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e4 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e3 @ ( e5 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e3 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e3 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e3 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e3 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e3 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e2 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e2 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e2 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e2 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e2 @ ( e1 @ op ) ) )
    & ( ( e1 @ ( e5 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e1 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e1 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e1 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e1 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e1 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e0 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e0 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e0 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e0 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e0 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e0 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e0 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e0 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e0 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e0 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e0 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e0 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e0 @ ( e1 @ op ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).

thf(440,plain,
    ( ( ( e5 @ ( e6 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e6 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e6 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e6 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e6 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e6 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e6 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e6 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e6 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e6 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e6 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e6 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e6 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e6 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e6 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e6 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e6 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e6 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e6 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e6 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e6 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e5 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e5 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e5 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e5 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e5 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e5 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e5 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e5 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e4 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e4 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e3 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e3 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e3 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e2 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e3 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e2 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e1 @ ( e3 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e3 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e3 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e2 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e3 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e2 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e1 @ ( e2 @ op ) ) )
    & ( ( e5 @ ( e1 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e3 @ ( e1 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e3 @ ( e1 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e2 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e3 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e2 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e1 @ ( e1 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e6 @ ( e0 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e6 @ ( e0 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e6 @ ( e0 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e4 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e6 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e4 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e3 @ ( e0 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e6 @ ( e0 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e4 @ ( e0 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e3 @ ( e0 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e2 @ ( e0 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e6 @ ( e0 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e4 @ ( e0 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e3 @ ( e0 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e2 @ ( e0 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e1 @ ( e0 @ op ) ) )
    & ( ( e6 @ ( e5 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e6 @ ( e4 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e6 @ ( e4 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e6 @ ( e3 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e6 @ ( e3 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e6 @ ( e3 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e6 @ ( e2 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e6 @ ( e2 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e6 @ ( e2 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e6 @ ( e2 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e6 @ ( e1 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e6 @ ( e1 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e6 @ ( e1 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e6 @ ( e1 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e6 @ ( e1 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e6 @ ( e0 @ op ) )
     != ( e6 @ ( e6 @ op ) ) )
    & ( ( e6 @ ( e0 @ op ) )
     != ( e6 @ ( e5 @ op ) ) )
    & ( ( e6 @ ( e0 @ op ) )
     != ( e6 @ ( e4 @ op ) ) )
    & ( ( e6 @ ( e0 @ op ) )
     != ( e6 @ ( e3 @ op ) ) )
    & ( ( e6 @ ( e0 @ op ) )
     != ( e6 @ ( e2 @ op ) ) )
    & ( ( e6 @ ( e0 @ op ) )
     != ( e6 @ ( e1 @ op ) ) )
    & ( ( e5 @ ( e5 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e4 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e4 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e3 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e3 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e3 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e5 @ ( e1 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e1 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e1 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e1 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e5 @ ( e1 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e5 @ ( e6 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e5 @ ( e0 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e4 @ ( e5 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e4 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e4 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e4 @ ( e6 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e3 @ ( e5 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e3 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e3 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e3 @ ( e6 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e3 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e3 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e3 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e2 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e2 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e2 @ ( e6 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e2 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e2 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e2 @ ( e1 @ op ) ) )
    & ( ( e1 @ ( e5 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e4 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e1 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e1 @ op ) )
     != ( e1 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e1 @ ( e6 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e1 @ ( e3 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e1 @ ( e2 @ op ) ) )
    & ( ( e1 @ ( e0 @ op ) )
     != ( e1 @ ( e1 @ op ) ) )
    & ( ( e0 @ ( e5 @ op ) )
     != ( e0 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e0 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e4 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e0 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e0 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e0 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e0 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e0 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e1 @ op ) )
     != ( e0 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e0 @ ( e6 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e0 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e0 @ ( e3 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e0 @ ( e2 @ op ) ) )
    & ( ( e0 @ ( e0 @ op ) )
     != ( e0 @ ( e1 @ op ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).

thf(3,axiom,
    ( ( ( ( e6 @ ( e6 @ op ) )
        = e6 )
      | ( ( e6 @ ( e6 @ op ) )
        = e5 )
      | ( ( e6 @ ( e6 @ op ) )
        = e4 )
      | ( ( e6 @ ( e6 @ op ) )
        = e3 )
      | ( ( e6 @ ( e6 @ op ) )
        = e2 )
      | ( ( e6 @ ( e6 @ op ) )
        = e1 )
      | ( ( e6 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e6 )
      | ( ( e5 @ ( e6 @ op ) )
        = e5 )
      | ( ( e5 @ ( e6 @ op ) )
        = e4 )
      | ( ( e5 @ ( e6 @ op ) )
        = e3 )
      | ( ( e5 @ ( e6 @ op ) )
        = e2 )
      | ( ( e5 @ ( e6 @ op ) )
        = e1 )
      | ( ( e5 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e6 )
      | ( ( e4 @ ( e6 @ op ) )
        = e5 )
      | ( ( e4 @ ( e6 @ op ) )
        = e4 )
      | ( ( e4 @ ( e6 @ op ) )
        = e3 )
      | ( ( e4 @ ( e6 @ op ) )
        = e2 )
      | ( ( e4 @ ( e6 @ op ) )
        = e1 )
      | ( ( e4 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e6 )
      | ( ( e3 @ ( e6 @ op ) )
        = e5 )
      | ( ( e3 @ ( e6 @ op ) )
        = e4 )
      | ( ( e3 @ ( e6 @ op ) )
        = e3 )
      | ( ( e3 @ ( e6 @ op ) )
        = e2 )
      | ( ( e3 @ ( e6 @ op ) )
        = e1 )
      | ( ( e3 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e6 )
      | ( ( e2 @ ( e6 @ op ) )
        = e5 )
      | ( ( e2 @ ( e6 @ op ) )
        = e4 )
      | ( ( e2 @ ( e6 @ op ) )
        = e3 )
      | ( ( e2 @ ( e6 @ op ) )
        = e2 )
      | ( ( e2 @ ( e6 @ op ) )
        = e1 )
      | ( ( e2 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e6 )
      | ( ( e1 @ ( e6 @ op ) )
        = e5 )
      | ( ( e1 @ ( e6 @ op ) )
        = e4 )
      | ( ( e1 @ ( e6 @ op ) )
        = e3 )
      | ( ( e1 @ ( e6 @ op ) )
        = e2 )
      | ( ( e1 @ ( e6 @ op ) )
        = e1 )
      | ( ( e1 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e6 )
      | ( ( e0 @ ( e6 @ op ) )
        = e5 )
      | ( ( e0 @ ( e6 @ op ) )
        = e4 )
      | ( ( e0 @ ( e6 @ op ) )
        = e3 )
      | ( ( e0 @ ( e6 @ op ) )
        = e2 )
      | ( ( e0 @ ( e6 @ op ) )
        = e1 )
      | ( ( e0 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e6 )
      | ( ( e6 @ ( e5 @ op ) )
        = e5 )
      | ( ( e6 @ ( e5 @ op ) )
        = e4 )
      | ( ( e6 @ ( e5 @ op ) )
        = e3 )
      | ( ( e6 @ ( e5 @ op ) )
        = e2 )
      | ( ( e6 @ ( e5 @ op ) )
        = e1 )
      | ( ( e6 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e5 @ op ) )
        = e6 )
      | ( ( e5 @ ( e5 @ op ) )
        = e5 )
      | ( ( e5 @ ( e5 @ op ) )
        = e4 )
      | ( ( e5 @ ( e5 @ op ) )
        = e3 )
      | ( ( e5 @ ( e5 @ op ) )
        = e2 )
      | ( ( e5 @ ( e5 @ op ) )
        = e1 )
      | ( ( e5 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e5 @ op ) )
        = e6 )
      | ( ( e4 @ ( e5 @ op ) )
        = e5 )
      | ( ( e4 @ ( e5 @ op ) )
        = e4 )
      | ( ( e4 @ ( e5 @ op ) )
        = e3 )
      | ( ( e4 @ ( e5 @ op ) )
        = e2 )
      | ( ( e4 @ ( e5 @ op ) )
        = e1 )
      | ( ( e4 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e5 @ op ) )
        = e6 )
      | ( ( e3 @ ( e5 @ op ) )
        = e5 )
      | ( ( e3 @ ( e5 @ op ) )
        = e4 )
      | ( ( e3 @ ( e5 @ op ) )
        = e3 )
      | ( ( e3 @ ( e5 @ op ) )
        = e2 )
      | ( ( e3 @ ( e5 @ op ) )
        = e1 )
      | ( ( e3 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e5 @ op ) )
        = e6 )
      | ( ( e2 @ ( e5 @ op ) )
        = e5 )
      | ( ( e2 @ ( e5 @ op ) )
        = e4 )
      | ( ( e2 @ ( e5 @ op ) )
        = e3 )
      | ( ( e2 @ ( e5 @ op ) )
        = e2 )
      | ( ( e2 @ ( e5 @ op ) )
        = e1 )
      | ( ( e2 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e5 @ op ) )
        = e6 )
      | ( ( e1 @ ( e5 @ op ) )
        = e5 )
      | ( ( e1 @ ( e5 @ op ) )
        = e4 )
      | ( ( e1 @ ( e5 @ op ) )
        = e3 )
      | ( ( e1 @ ( e5 @ op ) )
        = e2 )
      | ( ( e1 @ ( e5 @ op ) )
        = e1 )
      | ( ( e1 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e5 @ op ) )
        = e6 )
      | ( ( e0 @ ( e5 @ op ) )
        = e5 )
      | ( ( e0 @ ( e5 @ op ) )
        = e4 )
      | ( ( e0 @ ( e5 @ op ) )
        = e3 )
      | ( ( e0 @ ( e5 @ op ) )
        = e2 )
      | ( ( e0 @ ( e5 @ op ) )
        = e1 )
      | ( ( e0 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e6 )
      | ( ( e6 @ ( e4 @ op ) )
        = e5 )
      | ( ( e6 @ ( e4 @ op ) )
        = e4 )
      | ( ( e6 @ ( e4 @ op ) )
        = e3 )
      | ( ( e6 @ ( e4 @ op ) )
        = e2 )
      | ( ( e6 @ ( e4 @ op ) )
        = e1 )
      | ( ( e6 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e4 @ op ) )
        = e6 )
      | ( ( e5 @ ( e4 @ op ) )
        = e5 )
      | ( ( e5 @ ( e4 @ op ) )
        = e4 )
      | ( ( e5 @ ( e4 @ op ) )
        = e3 )
      | ( ( e5 @ ( e4 @ op ) )
        = e2 )
      | ( ( e5 @ ( e4 @ op ) )
        = e1 )
      | ( ( e5 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e4 @ op ) )
        = e6 )
      | ( ( e4 @ ( e4 @ op ) )
        = e5 )
      | ( ( e4 @ ( e4 @ op ) )
        = e4 )
      | ( ( e4 @ ( e4 @ op ) )
        = e3 )
      | ( ( e4 @ ( e4 @ op ) )
        = e2 )
      | ( ( e4 @ ( e4 @ op ) )
        = e1 )
      | ( ( e4 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e4 @ op ) )
        = e6 )
      | ( ( e3 @ ( e4 @ op ) )
        = e5 )
      | ( ( e3 @ ( e4 @ op ) )
        = e4 )
      | ( ( e3 @ ( e4 @ op ) )
        = e3 )
      | ( ( e3 @ ( e4 @ op ) )
        = e2 )
      | ( ( e3 @ ( e4 @ op ) )
        = e1 )
      | ( ( e3 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e4 @ op ) )
        = e6 )
      | ( ( e2 @ ( e4 @ op ) )
        = e5 )
      | ( ( e2 @ ( e4 @ op ) )
        = e4 )
      | ( ( e2 @ ( e4 @ op ) )
        = e3 )
      | ( ( e2 @ ( e4 @ op ) )
        = e2 )
      | ( ( e2 @ ( e4 @ op ) )
        = e1 )
      | ( ( e2 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e4 @ op ) )
        = e6 )
      | ( ( e1 @ ( e4 @ op ) )
        = e5 )
      | ( ( e1 @ ( e4 @ op ) )
        = e4 )
      | ( ( e1 @ ( e4 @ op ) )
        = e3 )
      | ( ( e1 @ ( e4 @ op ) )
        = e2 )
      | ( ( e1 @ ( e4 @ op ) )
        = e1 )
      | ( ( e1 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e4 @ op ) )
        = e6 )
      | ( ( e0 @ ( e4 @ op ) )
        = e5 )
      | ( ( e0 @ ( e4 @ op ) )
        = e4 )
      | ( ( e0 @ ( e4 @ op ) )
        = e3 )
      | ( ( e0 @ ( e4 @ op ) )
        = e2 )
      | ( ( e0 @ ( e4 @ op ) )
        = e1 )
      | ( ( e0 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e6 )
      | ( ( e6 @ ( e3 @ op ) )
        = e5 )
      | ( ( e6 @ ( e3 @ op ) )
        = e4 )
      | ( ( e6 @ ( e3 @ op ) )
        = e3 )
      | ( ( e6 @ ( e3 @ op ) )
        = e2 )
      | ( ( e6 @ ( e3 @ op ) )
        = e1 )
      | ( ( e6 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e3 @ op ) )
        = e6 )
      | ( ( e5 @ ( e3 @ op ) )
        = e5 )
      | ( ( e5 @ ( e3 @ op ) )
        = e4 )
      | ( ( e5 @ ( e3 @ op ) )
        = e3 )
      | ( ( e5 @ ( e3 @ op ) )
        = e2 )
      | ( ( e5 @ ( e3 @ op ) )
        = e1 )
      | ( ( e5 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e3 @ op ) )
        = e6 )
      | ( ( e4 @ ( e3 @ op ) )
        = e5 )
      | ( ( e4 @ ( e3 @ op ) )
        = e4 )
      | ( ( e4 @ ( e3 @ op ) )
        = e3 )
      | ( ( e4 @ ( e3 @ op ) )
        = e2 )
      | ( ( e4 @ ( e3 @ op ) )
        = e1 )
      | ( ( e4 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e3 @ op ) )
        = e6 )
      | ( ( e3 @ ( e3 @ op ) )
        = e5 )
      | ( ( e3 @ ( e3 @ op ) )
        = e4 )
      | ( ( e3 @ ( e3 @ op ) )
        = e3 )
      | ( ( e3 @ ( e3 @ op ) )
        = e2 )
      | ( ( e3 @ ( e3 @ op ) )
        = e1 )
      | ( ( e3 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e3 @ op ) )
        = e6 )
      | ( ( e2 @ ( e3 @ op ) )
        = e5 )
      | ( ( e2 @ ( e3 @ op ) )
        = e4 )
      | ( ( e2 @ ( e3 @ op ) )
        = e3 )
      | ( ( e2 @ ( e3 @ op ) )
        = e2 )
      | ( ( e2 @ ( e3 @ op ) )
        = e1 )
      | ( ( e2 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e3 @ op ) )
        = e6 )
      | ( ( e1 @ ( e3 @ op ) )
        = e5 )
      | ( ( e1 @ ( e3 @ op ) )
        = e4 )
      | ( ( e1 @ ( e3 @ op ) )
        = e3 )
      | ( ( e1 @ ( e3 @ op ) )
        = e2 )
      | ( ( e1 @ ( e3 @ op ) )
        = e1 )
      | ( ( e1 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e3 @ op ) )
        = e6 )
      | ( ( e0 @ ( e3 @ op ) )
        = e5 )
      | ( ( e0 @ ( e3 @ op ) )
        = e4 )
      | ( ( e0 @ ( e3 @ op ) )
        = e3 )
      | ( ( e0 @ ( e3 @ op ) )
        = e2 )
      | ( ( e0 @ ( e3 @ op ) )
        = e1 )
      | ( ( e0 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e6 )
      | ( ( e6 @ ( e2 @ op ) )
        = e5 )
      | ( ( e6 @ ( e2 @ op ) )
        = e4 )
      | ( ( e6 @ ( e2 @ op ) )
        = e3 )
      | ( ( e6 @ ( e2 @ op ) )
        = e2 )
      | ( ( e6 @ ( e2 @ op ) )
        = e1 )
      | ( ( e6 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e2 @ op ) )
        = e6 )
      | ( ( e5 @ ( e2 @ op ) )
        = e5 )
      | ( ( e5 @ ( e2 @ op ) )
        = e4 )
      | ( ( e5 @ ( e2 @ op ) )
        = e3 )
      | ( ( e5 @ ( e2 @ op ) )
        = e2 )
      | ( ( e5 @ ( e2 @ op ) )
        = e1 )
      | ( ( e5 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e2 @ op ) )
        = e6 )
      | ( ( e4 @ ( e2 @ op ) )
        = e5 )
      | ( ( e4 @ ( e2 @ op ) )
        = e4 )
      | ( ( e4 @ ( e2 @ op ) )
        = e3 )
      | ( ( e4 @ ( e2 @ op ) )
        = e2 )
      | ( ( e4 @ ( e2 @ op ) )
        = e1 )
      | ( ( e4 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e2 @ op ) )
        = e6 )
      | ( ( e3 @ ( e2 @ op ) )
        = e5 )
      | ( ( e3 @ ( e2 @ op ) )
        = e4 )
      | ( ( e3 @ ( e2 @ op ) )
        = e3 )
      | ( ( e3 @ ( e2 @ op ) )
        = e2 )
      | ( ( e3 @ ( e2 @ op ) )
        = e1 )
      | ( ( e3 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e2 @ op ) )
        = e6 )
      | ( ( e2 @ ( e2 @ op ) )
        = e5 )
      | ( ( e2 @ ( e2 @ op ) )
        = e4 )
      | ( ( e2 @ ( e2 @ op ) )
        = e3 )
      | ( ( e2 @ ( e2 @ op ) )
        = e2 )
      | ( ( e2 @ ( e2 @ op ) )
        = e1 )
      | ( ( e2 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e2 @ op ) )
        = e6 )
      | ( ( e1 @ ( e2 @ op ) )
        = e5 )
      | ( ( e1 @ ( e2 @ op ) )
        = e4 )
      | ( ( e1 @ ( e2 @ op ) )
        = e3 )
      | ( ( e1 @ ( e2 @ op ) )
        = e2 )
      | ( ( e1 @ ( e2 @ op ) )
        = e1 )
      | ( ( e1 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e2 @ op ) )
        = e6 )
      | ( ( e0 @ ( e2 @ op ) )
        = e5 )
      | ( ( e0 @ ( e2 @ op ) )
        = e4 )
      | ( ( e0 @ ( e2 @ op ) )
        = e3 )
      | ( ( e0 @ ( e2 @ op ) )
        = e2 )
      | ( ( e0 @ ( e2 @ op ) )
        = e1 )
      | ( ( e0 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e6 )
      | ( ( e6 @ ( e1 @ op ) )
        = e5 )
      | ( ( e6 @ ( e1 @ op ) )
        = e4 )
      | ( ( e6 @ ( e1 @ op ) )
        = e3 )
      | ( ( e6 @ ( e1 @ op ) )
        = e2 )
      | ( ( e6 @ ( e1 @ op ) )
        = e1 )
      | ( ( e6 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e1 @ op ) )
        = e6 )
      | ( ( e5 @ ( e1 @ op ) )
        = e5 )
      | ( ( e5 @ ( e1 @ op ) )
        = e4 )
      | ( ( e5 @ ( e1 @ op ) )
        = e3 )
      | ( ( e5 @ ( e1 @ op ) )
        = e2 )
      | ( ( e5 @ ( e1 @ op ) )
        = e1 )
      | ( ( e5 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e1 @ op ) )
        = e6 )
      | ( ( e4 @ ( e1 @ op ) )
        = e5 )
      | ( ( e4 @ ( e1 @ op ) )
        = e4 )
      | ( ( e4 @ ( e1 @ op ) )
        = e3 )
      | ( ( e4 @ ( e1 @ op ) )
        = e2 )
      | ( ( e4 @ ( e1 @ op ) )
        = e1 )
      | ( ( e4 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e1 @ op ) )
        = e6 )
      | ( ( e3 @ ( e1 @ op ) )
        = e5 )
      | ( ( e3 @ ( e1 @ op ) )
        = e4 )
      | ( ( e3 @ ( e1 @ op ) )
        = e3 )
      | ( ( e3 @ ( e1 @ op ) )
        = e2 )
      | ( ( e3 @ ( e1 @ op ) )
        = e1 )
      | ( ( e3 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e1 @ op ) )
        = e6 )
      | ( ( e2 @ ( e1 @ op ) )
        = e5 )
      | ( ( e2 @ ( e1 @ op ) )
        = e4 )
      | ( ( e2 @ ( e1 @ op ) )
        = e3 )
      | ( ( e2 @ ( e1 @ op ) )
        = e2 )
      | ( ( e2 @ ( e1 @ op ) )
        = e1 )
      | ( ( e2 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e1 @ op ) )
        = e6 )
      | ( ( e1 @ ( e1 @ op ) )
        = e5 )
      | ( ( e1 @ ( e1 @ op ) )
        = e4 )
      | ( ( e1 @ ( e1 @ op ) )
        = e3 )
      | ( ( e1 @ ( e1 @ op ) )
        = e2 )
      | ( ( e1 @ ( e1 @ op ) )
        = e1 )
      | ( ( e1 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e1 @ op ) )
        = e6 )
      | ( ( e0 @ ( e1 @ op ) )
        = e5 )
      | ( ( e0 @ ( e1 @ op ) )
        = e4 )
      | ( ( e0 @ ( e1 @ op ) )
        = e3 )
      | ( ( e0 @ ( e1 @ op ) )
        = e2 )
      | ( ( e0 @ ( e1 @ op ) )
        = e1 )
      | ( ( e0 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e6 )
      | ( ( e6 @ ( e0 @ op ) )
        = e5 )
      | ( ( e6 @ ( e0 @ op ) )
        = e4 )
      | ( ( e6 @ ( e0 @ op ) )
        = e3 )
      | ( ( e6 @ ( e0 @ op ) )
        = e2 )
      | ( ( e6 @ ( e0 @ op ) )
        = e1 )
      | ( ( e6 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e0 @ op ) )
        = e6 )
      | ( ( e5 @ ( e0 @ op ) )
        = e5 )
      | ( ( e5 @ ( e0 @ op ) )
        = e4 )
      | ( ( e5 @ ( e0 @ op ) )
        = e3 )
      | ( ( e5 @ ( e0 @ op ) )
        = e2 )
      | ( ( e5 @ ( e0 @ op ) )
        = e1 )
      | ( ( e5 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e0 @ op ) )
        = e6 )
      | ( ( e4 @ ( e0 @ op ) )
        = e5 )
      | ( ( e4 @ ( e0 @ op ) )
        = e4 )
      | ( ( e4 @ ( e0 @ op ) )
        = e3 )
      | ( ( e4 @ ( e0 @ op ) )
        = e2 )
      | ( ( e4 @ ( e0 @ op ) )
        = e1 )
      | ( ( e4 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e0 @ op ) )
        = e6 )
      | ( ( e3 @ ( e0 @ op ) )
        = e5 )
      | ( ( e3 @ ( e0 @ op ) )
        = e4 )
      | ( ( e3 @ ( e0 @ op ) )
        = e3 )
      | ( ( e3 @ ( e0 @ op ) )
        = e2 )
      | ( ( e3 @ ( e0 @ op ) )
        = e1 )
      | ( ( e3 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e0 @ op ) )
        = e6 )
      | ( ( e2 @ ( e0 @ op ) )
        = e5 )
      | ( ( e2 @ ( e0 @ op ) )
        = e4 )
      | ( ( e2 @ ( e0 @ op ) )
        = e3 )
      | ( ( e2 @ ( e0 @ op ) )
        = e2 )
      | ( ( e2 @ ( e0 @ op ) )
        = e1 )
      | ( ( e2 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e0 @ op ) )
        = e6 )
      | ( ( e1 @ ( e0 @ op ) )
        = e5 )
      | ( ( e1 @ ( e0 @ op ) )
        = e4 )
      | ( ( e1 @ ( e0 @ op ) )
        = e3 )
      | ( ( e1 @ ( e0 @ op ) )
        = e2 )
      | ( ( e1 @ ( e0 @ op ) )
        = e1 )
      | ( ( e1 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e0 @ op ) )
        = e6 )
      | ( ( e0 @ ( e0 @ op ) )
        = e5 )
      | ( ( e0 @ ( e0 @ op ) )
        = e4 )
      | ( ( e0 @ ( e0 @ op ) )
        = e3 )
      | ( ( e0 @ ( e0 @ op ) )
        = e2 )
      | ( ( e0 @ ( e0 @ op ) )
        = e1 )
      | ( ( e0 @ ( e0 @ op ) )
        = e0 ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).

thf(42,plain,
    ( ( ( ( e6 @ ( e6 @ op ) )
        = e6 )
      | ( ( e6 @ ( e6 @ op ) )
        = e5 )
      | ( ( e6 @ ( e6 @ op ) )
        = e4 )
      | ( ( e6 @ ( e6 @ op ) )
        = e3 )
      | ( ( e6 @ ( e6 @ op ) )
        = e2 )
      | ( ( e6 @ ( e6 @ op ) )
        = e1 )
      | ( ( e6 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e6 )
      | ( ( e5 @ ( e6 @ op ) )
        = e5 )
      | ( ( e5 @ ( e6 @ op ) )
        = e4 )
      | ( ( e5 @ ( e6 @ op ) )
        = e3 )
      | ( ( e5 @ ( e6 @ op ) )
        = e2 )
      | ( ( e5 @ ( e6 @ op ) )
        = e1 )
      | ( ( e5 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e6 )
      | ( ( e4 @ ( e6 @ op ) )
        = e5 )
      | ( ( e4 @ ( e6 @ op ) )
        = e4 )
      | ( ( e4 @ ( e6 @ op ) )
        = e3 )
      | ( ( e4 @ ( e6 @ op ) )
        = e2 )
      | ( ( e4 @ ( e6 @ op ) )
        = e1 )
      | ( ( e4 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e6 )
      | ( ( e3 @ ( e6 @ op ) )
        = e5 )
      | ( ( e3 @ ( e6 @ op ) )
        = e4 )
      | ( ( e3 @ ( e6 @ op ) )
        = e3 )
      | ( ( e3 @ ( e6 @ op ) )
        = e2 )
      | ( ( e3 @ ( e6 @ op ) )
        = e1 )
      | ( ( e3 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e6 )
      | ( ( e2 @ ( e6 @ op ) )
        = e5 )
      | ( ( e2 @ ( e6 @ op ) )
        = e4 )
      | ( ( e2 @ ( e6 @ op ) )
        = e3 )
      | ( ( e2 @ ( e6 @ op ) )
        = e2 )
      | ( ( e2 @ ( e6 @ op ) )
        = e1 )
      | ( ( e2 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e6 )
      | ( ( e1 @ ( e6 @ op ) )
        = e5 )
      | ( ( e1 @ ( e6 @ op ) )
        = e4 )
      | ( ( e1 @ ( e6 @ op ) )
        = e3 )
      | ( ( e1 @ ( e6 @ op ) )
        = e2 )
      | ( ( e1 @ ( e6 @ op ) )
        = e1 )
      | ( ( e1 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e6 )
      | ( ( e0 @ ( e6 @ op ) )
        = e5 )
      | ( ( e0 @ ( e6 @ op ) )
        = e4 )
      | ( ( e0 @ ( e6 @ op ) )
        = e3 )
      | ( ( e0 @ ( e6 @ op ) )
        = e2 )
      | ( ( e0 @ ( e6 @ op ) )
        = e1 )
      | ( ( e0 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e6 )
      | ( ( e6 @ ( e5 @ op ) )
        = e5 )
      | ( ( e6 @ ( e5 @ op ) )
        = e4 )
      | ( ( e6 @ ( e5 @ op ) )
        = e3 )
      | ( ( e6 @ ( e5 @ op ) )
        = e2 )
      | ( ( e6 @ ( e5 @ op ) )
        = e1 )
      | ( ( e6 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e5 @ op ) )
        = e6 )
      | ( ( e5 @ ( e5 @ op ) )
        = e5 )
      | ( ( e5 @ ( e5 @ op ) )
        = e4 )
      | ( ( e5 @ ( e5 @ op ) )
        = e3 )
      | ( ( e5 @ ( e5 @ op ) )
        = e2 )
      | ( ( e5 @ ( e5 @ op ) )
        = e1 )
      | ( ( e5 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e5 @ op ) )
        = e6 )
      | ( ( e4 @ ( e5 @ op ) )
        = e5 )
      | ( ( e4 @ ( e5 @ op ) )
        = e4 )
      | ( ( e4 @ ( e5 @ op ) )
        = e3 )
      | ( ( e4 @ ( e5 @ op ) )
        = e2 )
      | ( ( e4 @ ( e5 @ op ) )
        = e1 )
      | ( ( e4 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e5 @ op ) )
        = e6 )
      | ( ( e3 @ ( e5 @ op ) )
        = e5 )
      | ( ( e3 @ ( e5 @ op ) )
        = e4 )
      | ( ( e3 @ ( e5 @ op ) )
        = e3 )
      | ( ( e3 @ ( e5 @ op ) )
        = e2 )
      | ( ( e3 @ ( e5 @ op ) )
        = e1 )
      | ( ( e3 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e5 @ op ) )
        = e6 )
      | ( ( e2 @ ( e5 @ op ) )
        = e5 )
      | ( ( e2 @ ( e5 @ op ) )
        = e4 )
      | ( ( e2 @ ( e5 @ op ) )
        = e3 )
      | ( ( e2 @ ( e5 @ op ) )
        = e2 )
      | ( ( e2 @ ( e5 @ op ) )
        = e1 )
      | ( ( e2 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e5 @ op ) )
        = e6 )
      | ( ( e1 @ ( e5 @ op ) )
        = e5 )
      | ( ( e1 @ ( e5 @ op ) )
        = e4 )
      | ( ( e1 @ ( e5 @ op ) )
        = e3 )
      | ( ( e1 @ ( e5 @ op ) )
        = e2 )
      | ( ( e1 @ ( e5 @ op ) )
        = e1 )
      | ( ( e1 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e5 @ op ) )
        = e6 )
      | ( ( e0 @ ( e5 @ op ) )
        = e5 )
      | ( ( e0 @ ( e5 @ op ) )
        = e4 )
      | ( ( e0 @ ( e5 @ op ) )
        = e3 )
      | ( ( e0 @ ( e5 @ op ) )
        = e2 )
      | ( ( e0 @ ( e5 @ op ) )
        = e1 )
      | ( ( e0 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e6 )
      | ( ( e6 @ ( e4 @ op ) )
        = e5 )
      | ( ( e6 @ ( e4 @ op ) )
        = e4 )
      | ( ( e6 @ ( e4 @ op ) )
        = e3 )
      | ( ( e6 @ ( e4 @ op ) )
        = e2 )
      | ( ( e6 @ ( e4 @ op ) )
        = e1 )
      | ( ( e6 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e4 @ op ) )
        = e6 )
      | ( ( e5 @ ( e4 @ op ) )
        = e5 )
      | ( ( e5 @ ( e4 @ op ) )
        = e4 )
      | ( ( e5 @ ( e4 @ op ) )
        = e3 )
      | ( ( e5 @ ( e4 @ op ) )
        = e2 )
      | ( ( e5 @ ( e4 @ op ) )
        = e1 )
      | ( ( e5 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e4 @ op ) )
        = e6 )
      | ( ( e4 @ ( e4 @ op ) )
        = e5 )
      | ( ( e4 @ ( e4 @ op ) )
        = e4 )
      | ( ( e4 @ ( e4 @ op ) )
        = e3 )
      | ( ( e4 @ ( e4 @ op ) )
        = e2 )
      | ( ( e4 @ ( e4 @ op ) )
        = e1 )
      | ( ( e4 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e4 @ op ) )
        = e6 )
      | ( ( e3 @ ( e4 @ op ) )
        = e5 )
      | ( ( e3 @ ( e4 @ op ) )
        = e4 )
      | ( ( e3 @ ( e4 @ op ) )
        = e3 )
      | ( ( e3 @ ( e4 @ op ) )
        = e2 )
      | ( ( e3 @ ( e4 @ op ) )
        = e1 )
      | ( ( e3 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e4 @ op ) )
        = e6 )
      | ( ( e2 @ ( e4 @ op ) )
        = e5 )
      | ( ( e2 @ ( e4 @ op ) )
        = e4 )
      | ( ( e2 @ ( e4 @ op ) )
        = e3 )
      | ( ( e2 @ ( e4 @ op ) )
        = e2 )
      | ( ( e2 @ ( e4 @ op ) )
        = e1 )
      | ( ( e2 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e4 @ op ) )
        = e6 )
      | ( ( e1 @ ( e4 @ op ) )
        = e5 )
      | ( ( e1 @ ( e4 @ op ) )
        = e4 )
      | ( ( e1 @ ( e4 @ op ) )
        = e3 )
      | ( ( e1 @ ( e4 @ op ) )
        = e2 )
      | ( ( e1 @ ( e4 @ op ) )
        = e1 )
      | ( ( e1 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e4 @ op ) )
        = e6 )
      | ( ( e0 @ ( e4 @ op ) )
        = e5 )
      | ( ( e0 @ ( e4 @ op ) )
        = e4 )
      | ( ( e0 @ ( e4 @ op ) )
        = e3 )
      | ( ( e0 @ ( e4 @ op ) )
        = e2 )
      | ( ( e0 @ ( e4 @ op ) )
        = e1 )
      | ( ( e0 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e6 )
      | ( ( e6 @ ( e3 @ op ) )
        = e5 )
      | ( ( e6 @ ( e3 @ op ) )
        = e4 )
      | ( ( e6 @ ( e3 @ op ) )
        = e3 )
      | ( ( e6 @ ( e3 @ op ) )
        = e2 )
      | ( ( e6 @ ( e3 @ op ) )
        = e1 )
      | ( ( e6 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e3 @ op ) )
        = e6 )
      | ( ( e5 @ ( e3 @ op ) )
        = e5 )
      | ( ( e5 @ ( e3 @ op ) )
        = e4 )
      | ( ( e5 @ ( e3 @ op ) )
        = e3 )
      | ( ( e5 @ ( e3 @ op ) )
        = e2 )
      | ( ( e5 @ ( e3 @ op ) )
        = e1 )
      | ( ( e5 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e3 @ op ) )
        = e6 )
      | ( ( e4 @ ( e3 @ op ) )
        = e5 )
      | ( ( e4 @ ( e3 @ op ) )
        = e4 )
      | ( ( e4 @ ( e3 @ op ) )
        = e3 )
      | ( ( e4 @ ( e3 @ op ) )
        = e2 )
      | ( ( e4 @ ( e3 @ op ) )
        = e1 )
      | ( ( e4 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e3 @ op ) )
        = e6 )
      | ( ( e3 @ ( e3 @ op ) )
        = e5 )
      | ( ( e3 @ ( e3 @ op ) )
        = e4 )
      | ( ( e3 @ ( e3 @ op ) )
        = e3 )
      | ( ( e3 @ ( e3 @ op ) )
        = e2 )
      | ( ( e3 @ ( e3 @ op ) )
        = e1 )
      | ( ( e3 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e3 @ op ) )
        = e6 )
      | ( ( e2 @ ( e3 @ op ) )
        = e5 )
      | ( ( e2 @ ( e3 @ op ) )
        = e4 )
      | ( ( e2 @ ( e3 @ op ) )
        = e3 )
      | ( ( e2 @ ( e3 @ op ) )
        = e2 )
      | ( ( e2 @ ( e3 @ op ) )
        = e1 )
      | ( ( e2 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e3 @ op ) )
        = e6 )
      | ( ( e1 @ ( e3 @ op ) )
        = e5 )
      | ( ( e1 @ ( e3 @ op ) )
        = e4 )
      | ( ( e1 @ ( e3 @ op ) )
        = e3 )
      | ( ( e1 @ ( e3 @ op ) )
        = e2 )
      | ( ( e1 @ ( e3 @ op ) )
        = e1 )
      | ( ( e1 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e3 @ op ) )
        = e6 )
      | ( ( e0 @ ( e3 @ op ) )
        = e5 )
      | ( ( e0 @ ( e3 @ op ) )
        = e4 )
      | ( ( e0 @ ( e3 @ op ) )
        = e3 )
      | ( ( e0 @ ( e3 @ op ) )
        = e2 )
      | ( ( e0 @ ( e3 @ op ) )
        = e1 )
      | ( ( e0 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e6 )
      | ( ( e6 @ ( e2 @ op ) )
        = e5 )
      | ( ( e6 @ ( e2 @ op ) )
        = e4 )
      | ( ( e6 @ ( e2 @ op ) )
        = e3 )
      | ( ( e6 @ ( e2 @ op ) )
        = e2 )
      | ( ( e6 @ ( e2 @ op ) )
        = e1 )
      | ( ( e6 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e2 @ op ) )
        = e6 )
      | ( ( e5 @ ( e2 @ op ) )
        = e5 )
      | ( ( e5 @ ( e2 @ op ) )
        = e4 )
      | ( ( e5 @ ( e2 @ op ) )
        = e3 )
      | ( ( e5 @ ( e2 @ op ) )
        = e2 )
      | ( ( e5 @ ( e2 @ op ) )
        = e1 )
      | ( ( e5 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e2 @ op ) )
        = e6 )
      | ( ( e4 @ ( e2 @ op ) )
        = e5 )
      | ( ( e4 @ ( e2 @ op ) )
        = e4 )
      | ( ( e4 @ ( e2 @ op ) )
        = e3 )
      | ( ( e4 @ ( e2 @ op ) )
        = e2 )
      | ( ( e4 @ ( e2 @ op ) )
        = e1 )
      | ( ( e4 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e2 @ op ) )
        = e6 )
      | ( ( e3 @ ( e2 @ op ) )
        = e5 )
      | ( ( e3 @ ( e2 @ op ) )
        = e4 )
      | ( ( e3 @ ( e2 @ op ) )
        = e3 )
      | ( ( e3 @ ( e2 @ op ) )
        = e2 )
      | ( ( e3 @ ( e2 @ op ) )
        = e1 )
      | ( ( e3 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e2 @ op ) )
        = e6 )
      | ( ( e2 @ ( e2 @ op ) )
        = e5 )
      | ( ( e2 @ ( e2 @ op ) )
        = e4 )
      | ( ( e2 @ ( e2 @ op ) )
        = e3 )
      | ( ( e2 @ ( e2 @ op ) )
        = e2 )
      | ( ( e2 @ ( e2 @ op ) )
        = e1 )
      | ( ( e2 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e2 @ op ) )
        = e6 )
      | ( ( e1 @ ( e2 @ op ) )
        = e5 )
      | ( ( e1 @ ( e2 @ op ) )
        = e4 )
      | ( ( e1 @ ( e2 @ op ) )
        = e3 )
      | ( ( e1 @ ( e2 @ op ) )
        = e2 )
      | ( ( e1 @ ( e2 @ op ) )
        = e1 )
      | ( ( e1 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e2 @ op ) )
        = e6 )
      | ( ( e0 @ ( e2 @ op ) )
        = e5 )
      | ( ( e0 @ ( e2 @ op ) )
        = e4 )
      | ( ( e0 @ ( e2 @ op ) )
        = e3 )
      | ( ( e0 @ ( e2 @ op ) )
        = e2 )
      | ( ( e0 @ ( e2 @ op ) )
        = e1 )
      | ( ( e0 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e6 )
      | ( ( e6 @ ( e1 @ op ) )
        = e5 )
      | ( ( e6 @ ( e1 @ op ) )
        = e4 )
      | ( ( e6 @ ( e1 @ op ) )
        = e3 )
      | ( ( e6 @ ( e1 @ op ) )
        = e2 )
      | ( ( e6 @ ( e1 @ op ) )
        = e1 )
      | ( ( e6 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e1 @ op ) )
        = e6 )
      | ( ( e5 @ ( e1 @ op ) )
        = e5 )
      | ( ( e5 @ ( e1 @ op ) )
        = e4 )
      | ( ( e5 @ ( e1 @ op ) )
        = e3 )
      | ( ( e5 @ ( e1 @ op ) )
        = e2 )
      | ( ( e5 @ ( e1 @ op ) )
        = e1 )
      | ( ( e5 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e1 @ op ) )
        = e6 )
      | ( ( e4 @ ( e1 @ op ) )
        = e5 )
      | ( ( e4 @ ( e1 @ op ) )
        = e4 )
      | ( ( e4 @ ( e1 @ op ) )
        = e3 )
      | ( ( e4 @ ( e1 @ op ) )
        = e2 )
      | ( ( e4 @ ( e1 @ op ) )
        = e1 )
      | ( ( e4 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e1 @ op ) )
        = e6 )
      | ( ( e3 @ ( e1 @ op ) )
        = e5 )
      | ( ( e3 @ ( e1 @ op ) )
        = e4 )
      | ( ( e3 @ ( e1 @ op ) )
        = e3 )
      | ( ( e3 @ ( e1 @ op ) )
        = e2 )
      | ( ( e3 @ ( e1 @ op ) )
        = e1 )
      | ( ( e3 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e1 @ op ) )
        = e6 )
      | ( ( e2 @ ( e1 @ op ) )
        = e5 )
      | ( ( e2 @ ( e1 @ op ) )
        = e4 )
      | ( ( e2 @ ( e1 @ op ) )
        = e3 )
      | ( ( e2 @ ( e1 @ op ) )
        = e2 )
      | ( ( e2 @ ( e1 @ op ) )
        = e1 )
      | ( ( e2 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e1 @ op ) )
        = e6 )
      | ( ( e1 @ ( e1 @ op ) )
        = e5 )
      | ( ( e1 @ ( e1 @ op ) )
        = e4 )
      | ( ( e1 @ ( e1 @ op ) )
        = e3 )
      | ( ( e1 @ ( e1 @ op ) )
        = e2 )
      | ( ( e1 @ ( e1 @ op ) )
        = e1 )
      | ( ( e1 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e1 @ op ) )
        = e6 )
      | ( ( e0 @ ( e1 @ op ) )
        = e5 )
      | ( ( e0 @ ( e1 @ op ) )
        = e4 )
      | ( ( e0 @ ( e1 @ op ) )
        = e3 )
      | ( ( e0 @ ( e1 @ op ) )
        = e2 )
      | ( ( e0 @ ( e1 @ op ) )
        = e1 )
      | ( ( e0 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e6 )
      | ( ( e6 @ ( e0 @ op ) )
        = e5 )
      | ( ( e6 @ ( e0 @ op ) )
        = e4 )
      | ( ( e6 @ ( e0 @ op ) )
        = e3 )
      | ( ( e6 @ ( e0 @ op ) )
        = e2 )
      | ( ( e6 @ ( e0 @ op ) )
        = e1 )
      | ( ( e6 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e0 @ op ) )
        = e6 )
      | ( ( e5 @ ( e0 @ op ) )
        = e5 )
      | ( ( e5 @ ( e0 @ op ) )
        = e4 )
      | ( ( e5 @ ( e0 @ op ) )
        = e3 )
      | ( ( e5 @ ( e0 @ op ) )
        = e2 )
      | ( ( e5 @ ( e0 @ op ) )
        = e1 )
      | ( ( e5 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e0 @ op ) )
        = e6 )
      | ( ( e4 @ ( e0 @ op ) )
        = e5 )
      | ( ( e4 @ ( e0 @ op ) )
        = e4 )
      | ( ( e4 @ ( e0 @ op ) )
        = e3 )
      | ( ( e4 @ ( e0 @ op ) )
        = e2 )
      | ( ( e4 @ ( e0 @ op ) )
        = e1 )
      | ( ( e4 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e0 @ op ) )
        = e6 )
      | ( ( e3 @ ( e0 @ op ) )
        = e5 )
      | ( ( e3 @ ( e0 @ op ) )
        = e4 )
      | ( ( e3 @ ( e0 @ op ) )
        = e3 )
      | ( ( e3 @ ( e0 @ op ) )
        = e2 )
      | ( ( e3 @ ( e0 @ op ) )
        = e1 )
      | ( ( e3 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e0 @ op ) )
        = e6 )
      | ( ( e2 @ ( e0 @ op ) )
        = e5 )
      | ( ( e2 @ ( e0 @ op ) )
        = e4 )
      | ( ( e2 @ ( e0 @ op ) )
        = e3 )
      | ( ( e2 @ ( e0 @ op ) )
        = e2 )
      | ( ( e2 @ ( e0 @ op ) )
        = e1 )
      | ( ( e2 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e0 @ op ) )
        = e6 )
      | ( ( e1 @ ( e0 @ op ) )
        = e5 )
      | ( ( e1 @ ( e0 @ op ) )
        = e4 )
      | ( ( e1 @ ( e0 @ op ) )
        = e3 )
      | ( ( e1 @ ( e0 @ op ) )
        = e2 )
      | ( ( e1 @ ( e0 @ op ) )
        = e1 )
      | ( ( e1 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e0 @ op ) )
        = e6 )
      | ( ( e0 @ ( e0 @ op ) )
        = e5 )
      | ( ( e0 @ ( e0 @ op ) )
        = e4 )
      | ( ( e0 @ ( e0 @ op ) )
        = e3 )
      | ( ( e0 @ ( e0 @ op ) )
        = e2 )
      | ( ( e0 @ ( e0 @ op ) )
        = e1 )
      | ( ( e0 @ ( e0 @ op ) )
        = e0 ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).

thf(4,axiom,
    ( ( ( ( e6 @ ( e6 @ op ) )
        = e6 )
      | ( ( e6 @ ( e5 @ op ) )
        = e6 )
      | ( ( e6 @ ( e4 @ op ) )
        = e6 )
      | ( ( e6 @ ( e3 @ op ) )
        = e6 )
      | ( ( e6 @ ( e2 @ op ) )
        = e6 )
      | ( ( e6 @ ( e1 @ op ) )
        = e6 )
      | ( ( e6 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e6 )
      | ( ( e5 @ ( e6 @ op ) )
        = e6 )
      | ( ( e4 @ ( e6 @ op ) )
        = e6 )
      | ( ( e3 @ ( e6 @ op ) )
        = e6 )
      | ( ( e2 @ ( e6 @ op ) )
        = e6 )
      | ( ( e1 @ ( e6 @ op ) )
        = e6 )
      | ( ( e0 @ ( e6 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e5 )
      | ( ( e6 @ ( e5 @ op ) )
        = e5 )
      | ( ( e6 @ ( e4 @ op ) )
        = e5 )
      | ( ( e6 @ ( e3 @ op ) )
        = e5 )
      | ( ( e6 @ ( e2 @ op ) )
        = e5 )
      | ( ( e6 @ ( e1 @ op ) )
        = e5 )
      | ( ( e6 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e5 )
      | ( ( e5 @ ( e6 @ op ) )
        = e5 )
      | ( ( e4 @ ( e6 @ op ) )
        = e5 )
      | ( ( e3 @ ( e6 @ op ) )
        = e5 )
      | ( ( e2 @ ( e6 @ op ) )
        = e5 )
      | ( ( e1 @ ( e6 @ op ) )
        = e5 )
      | ( ( e0 @ ( e6 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e4 )
      | ( ( e6 @ ( e5 @ op ) )
        = e4 )
      | ( ( e6 @ ( e4 @ op ) )
        = e4 )
      | ( ( e6 @ ( e3 @ op ) )
        = e4 )
      | ( ( e6 @ ( e2 @ op ) )
        = e4 )
      | ( ( e6 @ ( e1 @ op ) )
        = e4 )
      | ( ( e6 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e4 )
      | ( ( e5 @ ( e6 @ op ) )
        = e4 )
      | ( ( e4 @ ( e6 @ op ) )
        = e4 )
      | ( ( e3 @ ( e6 @ op ) )
        = e4 )
      | ( ( e2 @ ( e6 @ op ) )
        = e4 )
      | ( ( e1 @ ( e6 @ op ) )
        = e4 )
      | ( ( e0 @ ( e6 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e3 )
      | ( ( e6 @ ( e5 @ op ) )
        = e3 )
      | ( ( e6 @ ( e4 @ op ) )
        = e3 )
      | ( ( e6 @ ( e3 @ op ) )
        = e3 )
      | ( ( e6 @ ( e2 @ op ) )
        = e3 )
      | ( ( e6 @ ( e1 @ op ) )
        = e3 )
      | ( ( e6 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e3 )
      | ( ( e5 @ ( e6 @ op ) )
        = e3 )
      | ( ( e4 @ ( e6 @ op ) )
        = e3 )
      | ( ( e3 @ ( e6 @ op ) )
        = e3 )
      | ( ( e2 @ ( e6 @ op ) )
        = e3 )
      | ( ( e1 @ ( e6 @ op ) )
        = e3 )
      | ( ( e0 @ ( e6 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e2 )
      | ( ( e6 @ ( e5 @ op ) )
        = e2 )
      | ( ( e6 @ ( e4 @ op ) )
        = e2 )
      | ( ( e6 @ ( e3 @ op ) )
        = e2 )
      | ( ( e6 @ ( e2 @ op ) )
        = e2 )
      | ( ( e6 @ ( e1 @ op ) )
        = e2 )
      | ( ( e6 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e2 )
      | ( ( e5 @ ( e6 @ op ) )
        = e2 )
      | ( ( e4 @ ( e6 @ op ) )
        = e2 )
      | ( ( e3 @ ( e6 @ op ) )
        = e2 )
      | ( ( e2 @ ( e6 @ op ) )
        = e2 )
      | ( ( e1 @ ( e6 @ op ) )
        = e2 )
      | ( ( e0 @ ( e6 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e1 )
      | ( ( e6 @ ( e5 @ op ) )
        = e1 )
      | ( ( e6 @ ( e4 @ op ) )
        = e1 )
      | ( ( e6 @ ( e3 @ op ) )
        = e1 )
      | ( ( e6 @ ( e2 @ op ) )
        = e1 )
      | ( ( e6 @ ( e1 @ op ) )
        = e1 )
      | ( ( e6 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e1 )
      | ( ( e5 @ ( e6 @ op ) )
        = e1 )
      | ( ( e4 @ ( e6 @ op ) )
        = e1 )
      | ( ( e3 @ ( e6 @ op ) )
        = e1 )
      | ( ( e2 @ ( e6 @ op ) )
        = e1 )
      | ( ( e1 @ ( e6 @ op ) )
        = e1 )
      | ( ( e0 @ ( e6 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e0 )
      | ( ( e6 @ ( e5 @ op ) )
        = e0 )
      | ( ( e6 @ ( e4 @ op ) )
        = e0 )
      | ( ( e6 @ ( e3 @ op ) )
        = e0 )
      | ( ( e6 @ ( e2 @ op ) )
        = e0 )
      | ( ( e6 @ ( e1 @ op ) )
        = e0 )
      | ( ( e6 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e0 )
      | ( ( e5 @ ( e6 @ op ) )
        = e0 )
      | ( ( e4 @ ( e6 @ op ) )
        = e0 )
      | ( ( e3 @ ( e6 @ op ) )
        = e0 )
      | ( ( e2 @ ( e6 @ op ) )
        = e0 )
      | ( ( e1 @ ( e6 @ op ) )
        = e0 )
      | ( ( e0 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e6 )
      | ( ( e5 @ ( e5 @ op ) )
        = e6 )
      | ( ( e5 @ ( e4 @ op ) )
        = e6 )
      | ( ( e5 @ ( e3 @ op ) )
        = e6 )
      | ( ( e5 @ ( e2 @ op ) )
        = e6 )
      | ( ( e5 @ ( e1 @ op ) )
        = e6 )
      | ( ( e5 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e6 )
      | ( ( e5 @ ( e5 @ op ) )
        = e6 )
      | ( ( e4 @ ( e5 @ op ) )
        = e6 )
      | ( ( e3 @ ( e5 @ op ) )
        = e6 )
      | ( ( e2 @ ( e5 @ op ) )
        = e6 )
      | ( ( e1 @ ( e5 @ op ) )
        = e6 )
      | ( ( e0 @ ( e5 @ op ) )
        = e6 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e5 )
      | ( ( e5 @ ( e5 @ op ) )
        = e5 )
      | ( ( e5 @ ( e4 @ op ) )
        = e5 )
      | ( ( e5 @ ( e3 @ op ) )
        = e5 )
      | ( ( e5 @ ( e2 @ op ) )
        = e5 )
      | ( ( e5 @ ( e1 @ op ) )
        = e5 )
      | ( ( e5 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e5 )
      | ( ( e5 @ ( e5 @ op ) )
        = e5 )
      | ( ( e4 @ ( e5 @ op ) )
        = e5 )
      | ( ( e3 @ ( e5 @ op ) )
        = e5 )
      | ( ( e2 @ ( e5 @ op ) )
        = e5 )
      | ( ( e1 @ ( e5 @ op ) )
        = e5 )
      | ( ( e0 @ ( e5 @ op ) )
        = e5 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e4 )
      | ( ( e5 @ ( e5 @ op ) )
        = e4 )
      | ( ( e5 @ ( e4 @ op ) )
        = e4 )
      | ( ( e5 @ ( e3 @ op ) )
        = e4 )
      | ( ( e5 @ ( e2 @ op ) )
        = e4 )
      | ( ( e5 @ ( e1 @ op ) )
        = e4 )
      | ( ( e5 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e4 )
      | ( ( e5 @ ( e5 @ op ) )
        = e4 )
      | ( ( e4 @ ( e5 @ op ) )
        = e4 )
      | ( ( e3 @ ( e5 @ op ) )
        = e4 )
      | ( ( e2 @ ( e5 @ op ) )
        = e4 )
      | ( ( e1 @ ( e5 @ op ) )
        = e4 )
      | ( ( e0 @ ( e5 @ op ) )
        = e4 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e3 )
      | ( ( e5 @ ( e5 @ op ) )
        = e3 )
      | ( ( e5 @ ( e4 @ op ) )
        = e3 )
      | ( ( e5 @ ( e3 @ op ) )
        = e3 )
      | ( ( e5 @ ( e2 @ op ) )
        = e3 )
      | ( ( e5 @ ( e1 @ op ) )
        = e3 )
      | ( ( e5 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e3 )
      | ( ( e5 @ ( e5 @ op ) )
        = e3 )
      | ( ( e4 @ ( e5 @ op ) )
        = e3 )
      | ( ( e3 @ ( e5 @ op ) )
        = e3 )
      | ( ( e2 @ ( e5 @ op ) )
        = e3 )
      | ( ( e1 @ ( e5 @ op ) )
        = e3 )
      | ( ( e0 @ ( e5 @ op ) )
        = e3 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e2 )
      | ( ( e5 @ ( e5 @ op ) )
        = e2 )
      | ( ( e5 @ ( e4 @ op ) )
        = e2 )
      | ( ( e5 @ ( e3 @ op ) )
        = e2 )
      | ( ( e5 @ ( e2 @ op ) )
        = e2 )
      | ( ( e5 @ ( e1 @ op ) )
        = e2 )
      | ( ( e5 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e2 )
      | ( ( e5 @ ( e5 @ op ) )
        = e2 )
      | ( ( e4 @ ( e5 @ op ) )
        = e2 )
      | ( ( e3 @ ( e5 @ op ) )
        = e2 )
      | ( ( e2 @ ( e5 @ op ) )
        = e2 )
      | ( ( e1 @ ( e5 @ op ) )
        = e2 )
      | ( ( e0 @ ( e5 @ op ) )
        = e2 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e1 )
      | ( ( e5 @ ( e5 @ op ) )
        = e1 )
      | ( ( e5 @ ( e4 @ op ) )
        = e1 )
      | ( ( e5 @ ( e3 @ op ) )
        = e1 )
      | ( ( e5 @ ( e2 @ op ) )
        = e1 )
      | ( ( e5 @ ( e1 @ op ) )
        = e1 )
      | ( ( e5 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e1 )
      | ( ( e5 @ ( e5 @ op ) )
        = e1 )
      | ( ( e4 @ ( e5 @ op ) )
        = e1 )
      | ( ( e3 @ ( e5 @ op ) )
        = e1 )
      | ( ( e2 @ ( e5 @ op ) )
        = e1 )
      | ( ( e1 @ ( e5 @ op ) )
        = e1 )
      | ( ( e0 @ ( e5 @ op ) )
        = e1 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e0 )
      | ( ( e5 @ ( e5 @ op ) )
        = e0 )
      | ( ( e5 @ ( e4 @ op ) )
        = e0 )
      | ( ( e5 @ ( e3 @ op ) )
        = e0 )
      | ( ( e5 @ ( e2 @ op ) )
        = e0 )
      | ( ( e5 @ ( e1 @ op ) )
        = e0 )
      | ( ( e5 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e0 )
      | ( ( e5 @ ( e5 @ op ) )
        = e0 )
      | ( ( e4 @ ( e5 @ op ) )
        = e0 )
      | ( ( e3 @ ( e5 @ op ) )
        = e0 )
      | ( ( e2 @ ( e5 @ op ) )
        = e0 )
      | ( ( e1 @ ( e5 @ op ) )
        = e0 )
      | ( ( e0 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e6 )
      | ( ( e4 @ ( e5 @ op ) )
        = e6 )
      | ( ( e4 @ ( e4 @ op ) )
        = e6 )
      | ( ( e4 @ ( e3 @ op ) )
        = e6 )
      | ( ( e4 @ ( e2 @ op ) )
        = e6 )
      | ( ( e4 @ ( e1 @ op ) )
        = e6 )
      | ( ( e4 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e6 )
      | ( ( e5 @ ( e4 @ op ) )
        = e6 )
      | ( ( e4 @ ( e4 @ op ) )
        = e6 )
      | ( ( e3 @ ( e4 @ op ) )
        = e6 )
      | ( ( e2 @ ( e4 @ op ) )
        = e6 )
      | ( ( e1 @ ( e4 @ op ) )
        = e6 )
      | ( ( e0 @ ( e4 @ op ) )
        = e6 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e5 )
      | ( ( e4 @ ( e5 @ op ) )
        = e5 )
      | ( ( e4 @ ( e4 @ op ) )
        = e5 )
      | ( ( e4 @ ( e3 @ op ) )
        = e5 )
      | ( ( e4 @ ( e2 @ op ) )
        = e5 )
      | ( ( e4 @ ( e1 @ op ) )
        = e5 )
      | ( ( e4 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e5 )
      | ( ( e5 @ ( e4 @ op ) )
        = e5 )
      | ( ( e4 @ ( e4 @ op ) )
        = e5 )
      | ( ( e3 @ ( e4 @ op ) )
        = e5 )
      | ( ( e2 @ ( e4 @ op ) )
        = e5 )
      | ( ( e1 @ ( e4 @ op ) )
        = e5 )
      | ( ( e0 @ ( e4 @ op ) )
        = e5 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e4 )
      | ( ( e4 @ ( e5 @ op ) )
        = e4 )
      | ( ( e4 @ ( e4 @ op ) )
        = e4 )
      | ( ( e4 @ ( e3 @ op ) )
        = e4 )
      | ( ( e4 @ ( e2 @ op ) )
        = e4 )
      | ( ( e4 @ ( e1 @ op ) )
        = e4 )
      | ( ( e4 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e4 )
      | ( ( e5 @ ( e4 @ op ) )
        = e4 )
      | ( ( e4 @ ( e4 @ op ) )
        = e4 )
      | ( ( e3 @ ( e4 @ op ) )
        = e4 )
      | ( ( e2 @ ( e4 @ op ) )
        = e4 )
      | ( ( e1 @ ( e4 @ op ) )
        = e4 )
      | ( ( e0 @ ( e4 @ op ) )
        = e4 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e3 )
      | ( ( e4 @ ( e5 @ op ) )
        = e3 )
      | ( ( e4 @ ( e4 @ op ) )
        = e3 )
      | ( ( e4 @ ( e3 @ op ) )
        = e3 )
      | ( ( e4 @ ( e2 @ op ) )
        = e3 )
      | ( ( e4 @ ( e1 @ op ) )
        = e3 )
      | ( ( e4 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e3 )
      | ( ( e5 @ ( e4 @ op ) )
        = e3 )
      | ( ( e4 @ ( e4 @ op ) )
        = e3 )
      | ( ( e3 @ ( e4 @ op ) )
        = e3 )
      | ( ( e2 @ ( e4 @ op ) )
        = e3 )
      | ( ( e1 @ ( e4 @ op ) )
        = e3 )
      | ( ( e0 @ ( e4 @ op ) )
        = e3 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e2 )
      | ( ( e4 @ ( e5 @ op ) )
        = e2 )
      | ( ( e4 @ ( e4 @ op ) )
        = e2 )
      | ( ( e4 @ ( e3 @ op ) )
        = e2 )
      | ( ( e4 @ ( e2 @ op ) )
        = e2 )
      | ( ( e4 @ ( e1 @ op ) )
        = e2 )
      | ( ( e4 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e2 )
      | ( ( e5 @ ( e4 @ op ) )
        = e2 )
      | ( ( e4 @ ( e4 @ op ) )
        = e2 )
      | ( ( e3 @ ( e4 @ op ) )
        = e2 )
      | ( ( e2 @ ( e4 @ op ) )
        = e2 )
      | ( ( e1 @ ( e4 @ op ) )
        = e2 )
      | ( ( e0 @ ( e4 @ op ) )
        = e2 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e1 )
      | ( ( e4 @ ( e5 @ op ) )
        = e1 )
      | ( ( e4 @ ( e4 @ op ) )
        = e1 )
      | ( ( e4 @ ( e3 @ op ) )
        = e1 )
      | ( ( e4 @ ( e2 @ op ) )
        = e1 )
      | ( ( e4 @ ( e1 @ op ) )
        = e1 )
      | ( ( e4 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e1 )
      | ( ( e5 @ ( e4 @ op ) )
        = e1 )
      | ( ( e4 @ ( e4 @ op ) )
        = e1 )
      | ( ( e3 @ ( e4 @ op ) )
        = e1 )
      | ( ( e2 @ ( e4 @ op ) )
        = e1 )
      | ( ( e1 @ ( e4 @ op ) )
        = e1 )
      | ( ( e0 @ ( e4 @ op ) )
        = e1 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e0 )
      | ( ( e4 @ ( e5 @ op ) )
        = e0 )
      | ( ( e4 @ ( e4 @ op ) )
        = e0 )
      | ( ( e4 @ ( e3 @ op ) )
        = e0 )
      | ( ( e4 @ ( e2 @ op ) )
        = e0 )
      | ( ( e4 @ ( e1 @ op ) )
        = e0 )
      | ( ( e4 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e0 )
      | ( ( e5 @ ( e4 @ op ) )
        = e0 )
      | ( ( e4 @ ( e4 @ op ) )
        = e0 )
      | ( ( e3 @ ( e4 @ op ) )
        = e0 )
      | ( ( e2 @ ( e4 @ op ) )
        = e0 )
      | ( ( e1 @ ( e4 @ op ) )
        = e0 )
      | ( ( e0 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e6 )
      | ( ( e3 @ ( e5 @ op ) )
        = e6 )
      | ( ( e3 @ ( e4 @ op ) )
        = e6 )
      | ( ( e3 @ ( e3 @ op ) )
        = e6 )
      | ( ( e3 @ ( e2 @ op ) )
        = e6 )
      | ( ( e3 @ ( e1 @ op ) )
        = e6 )
      | ( ( e3 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e6 )
      | ( ( e5 @ ( e3 @ op ) )
        = e6 )
      | ( ( e4 @ ( e3 @ op ) )
        = e6 )
      | ( ( e3 @ ( e3 @ op ) )
        = e6 )
      | ( ( e2 @ ( e3 @ op ) )
        = e6 )
      | ( ( e1 @ ( e3 @ op ) )
        = e6 )
      | ( ( e0 @ ( e3 @ op ) )
        = e6 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e5 )
      | ( ( e3 @ ( e5 @ op ) )
        = e5 )
      | ( ( e3 @ ( e4 @ op ) )
        = e5 )
      | ( ( e3 @ ( e3 @ op ) )
        = e5 )
      | ( ( e3 @ ( e2 @ op ) )
        = e5 )
      | ( ( e3 @ ( e1 @ op ) )
        = e5 )
      | ( ( e3 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e5 )
      | ( ( e5 @ ( e3 @ op ) )
        = e5 )
      | ( ( e4 @ ( e3 @ op ) )
        = e5 )
      | ( ( e3 @ ( e3 @ op ) )
        = e5 )
      | ( ( e2 @ ( e3 @ op ) )
        = e5 )
      | ( ( e1 @ ( e3 @ op ) )
        = e5 )
      | ( ( e0 @ ( e3 @ op ) )
        = e5 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e4 )
      | ( ( e3 @ ( e5 @ op ) )
        = e4 )
      | ( ( e3 @ ( e4 @ op ) )
        = e4 )
      | ( ( e3 @ ( e3 @ op ) )
        = e4 )
      | ( ( e3 @ ( e2 @ op ) )
        = e4 )
      | ( ( e3 @ ( e1 @ op ) )
        = e4 )
      | ( ( e3 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e4 )
      | ( ( e5 @ ( e3 @ op ) )
        = e4 )
      | ( ( e4 @ ( e3 @ op ) )
        = e4 )
      | ( ( e3 @ ( e3 @ op ) )
        = e4 )
      | ( ( e2 @ ( e3 @ op ) )
        = e4 )
      | ( ( e1 @ ( e3 @ op ) )
        = e4 )
      | ( ( e0 @ ( e3 @ op ) )
        = e4 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e3 )
      | ( ( e3 @ ( e5 @ op ) )
        = e3 )
      | ( ( e3 @ ( e4 @ op ) )
        = e3 )
      | ( ( e3 @ ( e3 @ op ) )
        = e3 )
      | ( ( e3 @ ( e2 @ op ) )
        = e3 )
      | ( ( e3 @ ( e1 @ op ) )
        = e3 )
      | ( ( e3 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e3 )
      | ( ( e5 @ ( e3 @ op ) )
        = e3 )
      | ( ( e4 @ ( e3 @ op ) )
        = e3 )
      | ( ( e3 @ ( e3 @ op ) )
        = e3 )
      | ( ( e2 @ ( e3 @ op ) )
        = e3 )
      | ( ( e1 @ ( e3 @ op ) )
        = e3 )
      | ( ( e0 @ ( e3 @ op ) )
        = e3 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e2 )
      | ( ( e3 @ ( e5 @ op ) )
        = e2 )
      | ( ( e3 @ ( e4 @ op ) )
        = e2 )
      | ( ( e3 @ ( e3 @ op ) )
        = e2 )
      | ( ( e3 @ ( e2 @ op ) )
        = e2 )
      | ( ( e3 @ ( e1 @ op ) )
        = e2 )
      | ( ( e3 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e2 )
      | ( ( e5 @ ( e3 @ op ) )
        = e2 )
      | ( ( e4 @ ( e3 @ op ) )
        = e2 )
      | ( ( e3 @ ( e3 @ op ) )
        = e2 )
      | ( ( e2 @ ( e3 @ op ) )
        = e2 )
      | ( ( e1 @ ( e3 @ op ) )
        = e2 )
      | ( ( e0 @ ( e3 @ op ) )
        = e2 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e1 )
      | ( ( e3 @ ( e5 @ op ) )
        = e1 )
      | ( ( e3 @ ( e4 @ op ) )
        = e1 )
      | ( ( e3 @ ( e3 @ op ) )
        = e1 )
      | ( ( e3 @ ( e2 @ op ) )
        = e1 )
      | ( ( e3 @ ( e1 @ op ) )
        = e1 )
      | ( ( e3 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e1 )
      | ( ( e5 @ ( e3 @ op ) )
        = e1 )
      | ( ( e4 @ ( e3 @ op ) )
        = e1 )
      | ( ( e3 @ ( e3 @ op ) )
        = e1 )
      | ( ( e2 @ ( e3 @ op ) )
        = e1 )
      | ( ( e1 @ ( e3 @ op ) )
        = e1 )
      | ( ( e0 @ ( e3 @ op ) )
        = e1 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e0 )
      | ( ( e3 @ ( e5 @ op ) )
        = e0 )
      | ( ( e3 @ ( e4 @ op ) )
        = e0 )
      | ( ( e3 @ ( e3 @ op ) )
        = e0 )
      | ( ( e3 @ ( e2 @ op ) )
        = e0 )
      | ( ( e3 @ ( e1 @ op ) )
        = e0 )
      | ( ( e3 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e0 )
      | ( ( e5 @ ( e3 @ op ) )
        = e0 )
      | ( ( e4 @ ( e3 @ op ) )
        = e0 )
      | ( ( e3 @ ( e3 @ op ) )
        = e0 )
      | ( ( e2 @ ( e3 @ op ) )
        = e0 )
      | ( ( e1 @ ( e3 @ op ) )
        = e0 )
      | ( ( e0 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e6 )
      | ( ( e2 @ ( e5 @ op ) )
        = e6 )
      | ( ( e2 @ ( e4 @ op ) )
        = e6 )
      | ( ( e2 @ ( e3 @ op ) )
        = e6 )
      | ( ( e2 @ ( e2 @ op ) )
        = e6 )
      | ( ( e2 @ ( e1 @ op ) )
        = e6 )
      | ( ( e2 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e6 )
      | ( ( e5 @ ( e2 @ op ) )
        = e6 )
      | ( ( e4 @ ( e2 @ op ) )
        = e6 )
      | ( ( e3 @ ( e2 @ op ) )
        = e6 )
      | ( ( e2 @ ( e2 @ op ) )
        = e6 )
      | ( ( e1 @ ( e2 @ op ) )
        = e6 )
      | ( ( e0 @ ( e2 @ op ) )
        = e6 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e5 )
      | ( ( e2 @ ( e5 @ op ) )
        = e5 )
      | ( ( e2 @ ( e4 @ op ) )
        = e5 )
      | ( ( e2 @ ( e3 @ op ) )
        = e5 )
      | ( ( e2 @ ( e2 @ op ) )
        = e5 )
      | ( ( e2 @ ( e1 @ op ) )
        = e5 )
      | ( ( e2 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e5 )
      | ( ( e5 @ ( e2 @ op ) )
        = e5 )
      | ( ( e4 @ ( e2 @ op ) )
        = e5 )
      | ( ( e3 @ ( e2 @ op ) )
        = e5 )
      | ( ( e2 @ ( e2 @ op ) )
        = e5 )
      | ( ( e1 @ ( e2 @ op ) )
        = e5 )
      | ( ( e0 @ ( e2 @ op ) )
        = e5 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e4 )
      | ( ( e2 @ ( e5 @ op ) )
        = e4 )
      | ( ( e2 @ ( e4 @ op ) )
        = e4 )
      | ( ( e2 @ ( e3 @ op ) )
        = e4 )
      | ( ( e2 @ ( e2 @ op ) )
        = e4 )
      | ( ( e2 @ ( e1 @ op ) )
        = e4 )
      | ( ( e2 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e4 )
      | ( ( e5 @ ( e2 @ op ) )
        = e4 )
      | ( ( e4 @ ( e2 @ op ) )
        = e4 )
      | ( ( e3 @ ( e2 @ op ) )
        = e4 )
      | ( ( e2 @ ( e2 @ op ) )
        = e4 )
      | ( ( e1 @ ( e2 @ op ) )
        = e4 )
      | ( ( e0 @ ( e2 @ op ) )
        = e4 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e3 )
      | ( ( e2 @ ( e5 @ op ) )
        = e3 )
      | ( ( e2 @ ( e4 @ op ) )
        = e3 )
      | ( ( e2 @ ( e3 @ op ) )
        = e3 )
      | ( ( e2 @ ( e2 @ op ) )
        = e3 )
      | ( ( e2 @ ( e1 @ op ) )
        = e3 )
      | ( ( e2 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e3 )
      | ( ( e5 @ ( e2 @ op ) )
        = e3 )
      | ( ( e4 @ ( e2 @ op ) )
        = e3 )
      | ( ( e3 @ ( e2 @ op ) )
        = e3 )
      | ( ( e2 @ ( e2 @ op ) )
        = e3 )
      | ( ( e1 @ ( e2 @ op ) )
        = e3 )
      | ( ( e0 @ ( e2 @ op ) )
        = e3 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e2 )
      | ( ( e2 @ ( e5 @ op ) )
        = e2 )
      | ( ( e2 @ ( e4 @ op ) )
        = e2 )
      | ( ( e2 @ ( e3 @ op ) )
        = e2 )
      | ( ( e2 @ ( e2 @ op ) )
        = e2 )
      | ( ( e2 @ ( e1 @ op ) )
        = e2 )
      | ( ( e2 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e2 )
      | ( ( e5 @ ( e2 @ op ) )
        = e2 )
      | ( ( e4 @ ( e2 @ op ) )
        = e2 )
      | ( ( e3 @ ( e2 @ op ) )
        = e2 )
      | ( ( e2 @ ( e2 @ op ) )
        = e2 )
      | ( ( e1 @ ( e2 @ op ) )
        = e2 )
      | ( ( e0 @ ( e2 @ op ) )
        = e2 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e1 )
      | ( ( e2 @ ( e5 @ op ) )
        = e1 )
      | ( ( e2 @ ( e4 @ op ) )
        = e1 )
      | ( ( e2 @ ( e3 @ op ) )
        = e1 )
      | ( ( e2 @ ( e2 @ op ) )
        = e1 )
      | ( ( e2 @ ( e1 @ op ) )
        = e1 )
      | ( ( e2 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e1 )
      | ( ( e5 @ ( e2 @ op ) )
        = e1 )
      | ( ( e4 @ ( e2 @ op ) )
        = e1 )
      | ( ( e3 @ ( e2 @ op ) )
        = e1 )
      | ( ( e2 @ ( e2 @ op ) )
        = e1 )
      | ( ( e1 @ ( e2 @ op ) )
        = e1 )
      | ( ( e0 @ ( e2 @ op ) )
        = e1 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e0 )
      | ( ( e2 @ ( e5 @ op ) )
        = e0 )
      | ( ( e2 @ ( e4 @ op ) )
        = e0 )
      | ( ( e2 @ ( e3 @ op ) )
        = e0 )
      | ( ( e2 @ ( e2 @ op ) )
        = e0 )
      | ( ( e2 @ ( e1 @ op ) )
        = e0 )
      | ( ( e2 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e0 )
      | ( ( e5 @ ( e2 @ op ) )
        = e0 )
      | ( ( e4 @ ( e2 @ op ) )
        = e0 )
      | ( ( e3 @ ( e2 @ op ) )
        = e0 )
      | ( ( e2 @ ( e2 @ op ) )
        = e0 )
      | ( ( e1 @ ( e2 @ op ) )
        = e0 )
      | ( ( e0 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e6 )
      | ( ( e1 @ ( e5 @ op ) )
        = e6 )
      | ( ( e1 @ ( e4 @ op ) )
        = e6 )
      | ( ( e1 @ ( e3 @ op ) )
        = e6 )
      | ( ( e1 @ ( e2 @ op ) )
        = e6 )
      | ( ( e1 @ ( e1 @ op ) )
        = e6 )
      | ( ( e1 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e6 )
      | ( ( e5 @ ( e1 @ op ) )
        = e6 )
      | ( ( e4 @ ( e1 @ op ) )
        = e6 )
      | ( ( e3 @ ( e1 @ op ) )
        = e6 )
      | ( ( e2 @ ( e1 @ op ) )
        = e6 )
      | ( ( e1 @ ( e1 @ op ) )
        = e6 )
      | ( ( e0 @ ( e1 @ op ) )
        = e6 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e5 )
      | ( ( e1 @ ( e5 @ op ) )
        = e5 )
      | ( ( e1 @ ( e4 @ op ) )
        = e5 )
      | ( ( e1 @ ( e3 @ op ) )
        = e5 )
      | ( ( e1 @ ( e2 @ op ) )
        = e5 )
      | ( ( e1 @ ( e1 @ op ) )
        = e5 )
      | ( ( e1 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e5 )
      | ( ( e5 @ ( e1 @ op ) )
        = e5 )
      | ( ( e4 @ ( e1 @ op ) )
        = e5 )
      | ( ( e3 @ ( e1 @ op ) )
        = e5 )
      | ( ( e2 @ ( e1 @ op ) )
        = e5 )
      | ( ( e1 @ ( e1 @ op ) )
        = e5 )
      | ( ( e0 @ ( e1 @ op ) )
        = e5 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e4 )
      | ( ( e1 @ ( e5 @ op ) )
        = e4 )
      | ( ( e1 @ ( e4 @ op ) )
        = e4 )
      | ( ( e1 @ ( e3 @ op ) )
        = e4 )
      | ( ( e1 @ ( e2 @ op ) )
        = e4 )
      | ( ( e1 @ ( e1 @ op ) )
        = e4 )
      | ( ( e1 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e4 )
      | ( ( e5 @ ( e1 @ op ) )
        = e4 )
      | ( ( e4 @ ( e1 @ op ) )
        = e4 )
      | ( ( e3 @ ( e1 @ op ) )
        = e4 )
      | ( ( e2 @ ( e1 @ op ) )
        = e4 )
      | ( ( e1 @ ( e1 @ op ) )
        = e4 )
      | ( ( e0 @ ( e1 @ op ) )
        = e4 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e3 )
      | ( ( e1 @ ( e5 @ op ) )
        = e3 )
      | ( ( e1 @ ( e4 @ op ) )
        = e3 )
      | ( ( e1 @ ( e3 @ op ) )
        = e3 )
      | ( ( e1 @ ( e2 @ op ) )
        = e3 )
      | ( ( e1 @ ( e1 @ op ) )
        = e3 )
      | ( ( e1 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e3 )
      | ( ( e5 @ ( e1 @ op ) )
        = e3 )
      | ( ( e4 @ ( e1 @ op ) )
        = e3 )
      | ( ( e3 @ ( e1 @ op ) )
        = e3 )
      | ( ( e2 @ ( e1 @ op ) )
        = e3 )
      | ( ( e1 @ ( e1 @ op ) )
        = e3 )
      | ( ( e0 @ ( e1 @ op ) )
        = e3 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e2 )
      | ( ( e1 @ ( e5 @ op ) )
        = e2 )
      | ( ( e1 @ ( e4 @ op ) )
        = e2 )
      | ( ( e1 @ ( e3 @ op ) )
        = e2 )
      | ( ( e1 @ ( e2 @ op ) )
        = e2 )
      | ( ( e1 @ ( e1 @ op ) )
        = e2 )
      | ( ( e1 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e2 )
      | ( ( e5 @ ( e1 @ op ) )
        = e2 )
      | ( ( e4 @ ( e1 @ op ) )
        = e2 )
      | ( ( e3 @ ( e1 @ op ) )
        = e2 )
      | ( ( e2 @ ( e1 @ op ) )
        = e2 )
      | ( ( e1 @ ( e1 @ op ) )
        = e2 )
      | ( ( e0 @ ( e1 @ op ) )
        = e2 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e1 )
      | ( ( e1 @ ( e5 @ op ) )
        = e1 )
      | ( ( e1 @ ( e4 @ op ) )
        = e1 )
      | ( ( e1 @ ( e3 @ op ) )
        = e1 )
      | ( ( e1 @ ( e2 @ op ) )
        = e1 )
      | ( ( e1 @ ( e1 @ op ) )
        = e1 )
      | ( ( e1 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e1 )
      | ( ( e5 @ ( e1 @ op ) )
        = e1 )
      | ( ( e4 @ ( e1 @ op ) )
        = e1 )
      | ( ( e3 @ ( e1 @ op ) )
        = e1 )
      | ( ( e2 @ ( e1 @ op ) )
        = e1 )
      | ( ( e1 @ ( e1 @ op ) )
        = e1 )
      | ( ( e0 @ ( e1 @ op ) )
        = e1 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e0 )
      | ( ( e1 @ ( e5 @ op ) )
        = e0 )
      | ( ( e1 @ ( e4 @ op ) )
        = e0 )
      | ( ( e1 @ ( e3 @ op ) )
        = e0 )
      | ( ( e1 @ ( e2 @ op ) )
        = e0 )
      | ( ( e1 @ ( e1 @ op ) )
        = e0 )
      | ( ( e1 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e0 )
      | ( ( e5 @ ( e1 @ op ) )
        = e0 )
      | ( ( e4 @ ( e1 @ op ) )
        = e0 )
      | ( ( e3 @ ( e1 @ op ) )
        = e0 )
      | ( ( e2 @ ( e1 @ op ) )
        = e0 )
      | ( ( e1 @ ( e1 @ op ) )
        = e0 )
      | ( ( e0 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e6 )
      | ( ( e0 @ ( e5 @ op ) )
        = e6 )
      | ( ( e0 @ ( e4 @ op ) )
        = e6 )
      | ( ( e0 @ ( e3 @ op ) )
        = e6 )
      | ( ( e0 @ ( e2 @ op ) )
        = e6 )
      | ( ( e0 @ ( e1 @ op ) )
        = e6 )
      | ( ( e0 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e6 )
      | ( ( e5 @ ( e0 @ op ) )
        = e6 )
      | ( ( e4 @ ( e0 @ op ) )
        = e6 )
      | ( ( e3 @ ( e0 @ op ) )
        = e6 )
      | ( ( e2 @ ( e0 @ op ) )
        = e6 )
      | ( ( e1 @ ( e0 @ op ) )
        = e6 )
      | ( ( e0 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e5 )
      | ( ( e0 @ ( e5 @ op ) )
        = e5 )
      | ( ( e0 @ ( e4 @ op ) )
        = e5 )
      | ( ( e0 @ ( e3 @ op ) )
        = e5 )
      | ( ( e0 @ ( e2 @ op ) )
        = e5 )
      | ( ( e0 @ ( e1 @ op ) )
        = e5 )
      | ( ( e0 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e5 )
      | ( ( e5 @ ( e0 @ op ) )
        = e5 )
      | ( ( e4 @ ( e0 @ op ) )
        = e5 )
      | ( ( e3 @ ( e0 @ op ) )
        = e5 )
      | ( ( e2 @ ( e0 @ op ) )
        = e5 )
      | ( ( e1 @ ( e0 @ op ) )
        = e5 )
      | ( ( e0 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e4 )
      | ( ( e0 @ ( e5 @ op ) )
        = e4 )
      | ( ( e0 @ ( e4 @ op ) )
        = e4 )
      | ( ( e0 @ ( e3 @ op ) )
        = e4 )
      | ( ( e0 @ ( e2 @ op ) )
        = e4 )
      | ( ( e0 @ ( e1 @ op ) )
        = e4 )
      | ( ( e0 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e4 )
      | ( ( e5 @ ( e0 @ op ) )
        = e4 )
      | ( ( e4 @ ( e0 @ op ) )
        = e4 )
      | ( ( e3 @ ( e0 @ op ) )
        = e4 )
      | ( ( e2 @ ( e0 @ op ) )
        = e4 )
      | ( ( e1 @ ( e0 @ op ) )
        = e4 )
      | ( ( e0 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e3 )
      | ( ( e0 @ ( e5 @ op ) )
        = e3 )
      | ( ( e0 @ ( e4 @ op ) )
        = e3 )
      | ( ( e0 @ ( e3 @ op ) )
        = e3 )
      | ( ( e0 @ ( e2 @ op ) )
        = e3 )
      | ( ( e0 @ ( e1 @ op ) )
        = e3 )
      | ( ( e0 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e3 )
      | ( ( e5 @ ( e0 @ op ) )
        = e3 )
      | ( ( e4 @ ( e0 @ op ) )
        = e3 )
      | ( ( e3 @ ( e0 @ op ) )
        = e3 )
      | ( ( e2 @ ( e0 @ op ) )
        = e3 )
      | ( ( e1 @ ( e0 @ op ) )
        = e3 )
      | ( ( e0 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e2 )
      | ( ( e0 @ ( e5 @ op ) )
        = e2 )
      | ( ( e0 @ ( e4 @ op ) )
        = e2 )
      | ( ( e0 @ ( e3 @ op ) )
        = e2 )
      | ( ( e0 @ ( e2 @ op ) )
        = e2 )
      | ( ( e0 @ ( e1 @ op ) )
        = e2 )
      | ( ( e0 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e2 )
      | ( ( e5 @ ( e0 @ op ) )
        = e2 )
      | ( ( e4 @ ( e0 @ op ) )
        = e2 )
      | ( ( e3 @ ( e0 @ op ) )
        = e2 )
      | ( ( e2 @ ( e0 @ op ) )
        = e2 )
      | ( ( e1 @ ( e0 @ op ) )
        = e2 )
      | ( ( e0 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e1 )
      | ( ( e0 @ ( e5 @ op ) )
        = e1 )
      | ( ( e0 @ ( e4 @ op ) )
        = e1 )
      | ( ( e0 @ ( e3 @ op ) )
        = e1 )
      | ( ( e0 @ ( e2 @ op ) )
        = e1 )
      | ( ( e0 @ ( e1 @ op ) )
        = e1 )
      | ( ( e0 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e1 )
      | ( ( e5 @ ( e0 @ op ) )
        = e1 )
      | ( ( e4 @ ( e0 @ op ) )
        = e1 )
      | ( ( e3 @ ( e0 @ op ) )
        = e1 )
      | ( ( e2 @ ( e0 @ op ) )
        = e1 )
      | ( ( e1 @ ( e0 @ op ) )
        = e1 )
      | ( ( e0 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e0 )
      | ( ( e0 @ ( e5 @ op ) )
        = e0 )
      | ( ( e0 @ ( e4 @ op ) )
        = e0 )
      | ( ( e0 @ ( e3 @ op ) )
        = e0 )
      | ( ( e0 @ ( e2 @ op ) )
        = e0 )
      | ( ( e0 @ ( e1 @ op ) )
        = e0 )
      | ( ( e0 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e0 )
      | ( ( e5 @ ( e0 @ op ) )
        = e0 )
      | ( ( e4 @ ( e0 @ op ) )
        = e0 )
      | ( ( e3 @ ( e0 @ op ) )
        = e0 )
      | ( ( e2 @ ( e0 @ op ) )
        = e0 )
      | ( ( e1 @ ( e0 @ op ) )
        = e0 )
      | ( ( e0 @ ( e0 @ op ) )
        = e0 ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).

thf(142,plain,
    ( ( ( ( e6 @ ( e6 @ op ) )
        = e6 )
      | ( ( e6 @ ( e5 @ op ) )
        = e6 )
      | ( ( e6 @ ( e4 @ op ) )
        = e6 )
      | ( ( e6 @ ( e3 @ op ) )
        = e6 )
      | ( ( e6 @ ( e2 @ op ) )
        = e6 )
      | ( ( e6 @ ( e1 @ op ) )
        = e6 )
      | ( ( e6 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e6 )
      | ( ( e5 @ ( e6 @ op ) )
        = e6 )
      | ( ( e4 @ ( e6 @ op ) )
        = e6 )
      | ( ( e3 @ ( e6 @ op ) )
        = e6 )
      | ( ( e2 @ ( e6 @ op ) )
        = e6 )
      | ( ( e1 @ ( e6 @ op ) )
        = e6 )
      | ( ( e0 @ ( e6 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e5 )
      | ( ( e6 @ ( e5 @ op ) )
        = e5 )
      | ( ( e6 @ ( e4 @ op ) )
        = e5 )
      | ( ( e6 @ ( e3 @ op ) )
        = e5 )
      | ( ( e6 @ ( e2 @ op ) )
        = e5 )
      | ( ( e6 @ ( e1 @ op ) )
        = e5 )
      | ( ( e6 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e5 )
      | ( ( e5 @ ( e6 @ op ) )
        = e5 )
      | ( ( e4 @ ( e6 @ op ) )
        = e5 )
      | ( ( e3 @ ( e6 @ op ) )
        = e5 )
      | ( ( e2 @ ( e6 @ op ) )
        = e5 )
      | ( ( e1 @ ( e6 @ op ) )
        = e5 )
      | ( ( e0 @ ( e6 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e4 )
      | ( ( e6 @ ( e5 @ op ) )
        = e4 )
      | ( ( e6 @ ( e4 @ op ) )
        = e4 )
      | ( ( e6 @ ( e3 @ op ) )
        = e4 )
      | ( ( e6 @ ( e2 @ op ) )
        = e4 )
      | ( ( e6 @ ( e1 @ op ) )
        = e4 )
      | ( ( e6 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e4 )
      | ( ( e5 @ ( e6 @ op ) )
        = e4 )
      | ( ( e4 @ ( e6 @ op ) )
        = e4 )
      | ( ( e3 @ ( e6 @ op ) )
        = e4 )
      | ( ( e2 @ ( e6 @ op ) )
        = e4 )
      | ( ( e1 @ ( e6 @ op ) )
        = e4 )
      | ( ( e0 @ ( e6 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e3 )
      | ( ( e6 @ ( e5 @ op ) )
        = e3 )
      | ( ( e6 @ ( e4 @ op ) )
        = e3 )
      | ( ( e6 @ ( e3 @ op ) )
        = e3 )
      | ( ( e6 @ ( e2 @ op ) )
        = e3 )
      | ( ( e6 @ ( e1 @ op ) )
        = e3 )
      | ( ( e6 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e3 )
      | ( ( e5 @ ( e6 @ op ) )
        = e3 )
      | ( ( e4 @ ( e6 @ op ) )
        = e3 )
      | ( ( e3 @ ( e6 @ op ) )
        = e3 )
      | ( ( e2 @ ( e6 @ op ) )
        = e3 )
      | ( ( e1 @ ( e6 @ op ) )
        = e3 )
      | ( ( e0 @ ( e6 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e2 )
      | ( ( e6 @ ( e5 @ op ) )
        = e2 )
      | ( ( e6 @ ( e4 @ op ) )
        = e2 )
      | ( ( e6 @ ( e3 @ op ) )
        = e2 )
      | ( ( e6 @ ( e2 @ op ) )
        = e2 )
      | ( ( e6 @ ( e1 @ op ) )
        = e2 )
      | ( ( e6 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e2 )
      | ( ( e5 @ ( e6 @ op ) )
        = e2 )
      | ( ( e4 @ ( e6 @ op ) )
        = e2 )
      | ( ( e3 @ ( e6 @ op ) )
        = e2 )
      | ( ( e2 @ ( e6 @ op ) )
        = e2 )
      | ( ( e1 @ ( e6 @ op ) )
        = e2 )
      | ( ( e0 @ ( e6 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e1 )
      | ( ( e6 @ ( e5 @ op ) )
        = e1 )
      | ( ( e6 @ ( e4 @ op ) )
        = e1 )
      | ( ( e6 @ ( e3 @ op ) )
        = e1 )
      | ( ( e6 @ ( e2 @ op ) )
        = e1 )
      | ( ( e6 @ ( e1 @ op ) )
        = e1 )
      | ( ( e6 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e1 )
      | ( ( e5 @ ( e6 @ op ) )
        = e1 )
      | ( ( e4 @ ( e6 @ op ) )
        = e1 )
      | ( ( e3 @ ( e6 @ op ) )
        = e1 )
      | ( ( e2 @ ( e6 @ op ) )
        = e1 )
      | ( ( e1 @ ( e6 @ op ) )
        = e1 )
      | ( ( e0 @ ( e6 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e0 )
      | ( ( e6 @ ( e5 @ op ) )
        = e0 )
      | ( ( e6 @ ( e4 @ op ) )
        = e0 )
      | ( ( e6 @ ( e3 @ op ) )
        = e0 )
      | ( ( e6 @ ( e2 @ op ) )
        = e0 )
      | ( ( e6 @ ( e1 @ op ) )
        = e0 )
      | ( ( e6 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e6 @ op ) )
        = e0 )
      | ( ( e5 @ ( e6 @ op ) )
        = e0 )
      | ( ( e4 @ ( e6 @ op ) )
        = e0 )
      | ( ( e3 @ ( e6 @ op ) )
        = e0 )
      | ( ( e2 @ ( e6 @ op ) )
        = e0 )
      | ( ( e1 @ ( e6 @ op ) )
        = e0 )
      | ( ( e0 @ ( e6 @ op ) )
        = e0 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e6 )
      | ( ( e5 @ ( e5 @ op ) )
        = e6 )
      | ( ( e5 @ ( e4 @ op ) )
        = e6 )
      | ( ( e5 @ ( e3 @ op ) )
        = e6 )
      | ( ( e5 @ ( e2 @ op ) )
        = e6 )
      | ( ( e5 @ ( e1 @ op ) )
        = e6 )
      | ( ( e5 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e6 )
      | ( ( e5 @ ( e5 @ op ) )
        = e6 )
      | ( ( e4 @ ( e5 @ op ) )
        = e6 )
      | ( ( e3 @ ( e5 @ op ) )
        = e6 )
      | ( ( e2 @ ( e5 @ op ) )
        = e6 )
      | ( ( e1 @ ( e5 @ op ) )
        = e6 )
      | ( ( e0 @ ( e5 @ op ) )
        = e6 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e5 )
      | ( ( e5 @ ( e5 @ op ) )
        = e5 )
      | ( ( e5 @ ( e4 @ op ) )
        = e5 )
      | ( ( e5 @ ( e3 @ op ) )
        = e5 )
      | ( ( e5 @ ( e2 @ op ) )
        = e5 )
      | ( ( e5 @ ( e1 @ op ) )
        = e5 )
      | ( ( e5 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e5 )
      | ( ( e5 @ ( e5 @ op ) )
        = e5 )
      | ( ( e4 @ ( e5 @ op ) )
        = e5 )
      | ( ( e3 @ ( e5 @ op ) )
        = e5 )
      | ( ( e2 @ ( e5 @ op ) )
        = e5 )
      | ( ( e1 @ ( e5 @ op ) )
        = e5 )
      | ( ( e0 @ ( e5 @ op ) )
        = e5 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e4 )
      | ( ( e5 @ ( e5 @ op ) )
        = e4 )
      | ( ( e5 @ ( e4 @ op ) )
        = e4 )
      | ( ( e5 @ ( e3 @ op ) )
        = e4 )
      | ( ( e5 @ ( e2 @ op ) )
        = e4 )
      | ( ( e5 @ ( e1 @ op ) )
        = e4 )
      | ( ( e5 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e4 )
      | ( ( e5 @ ( e5 @ op ) )
        = e4 )
      | ( ( e4 @ ( e5 @ op ) )
        = e4 )
      | ( ( e3 @ ( e5 @ op ) )
        = e4 )
      | ( ( e2 @ ( e5 @ op ) )
        = e4 )
      | ( ( e1 @ ( e5 @ op ) )
        = e4 )
      | ( ( e0 @ ( e5 @ op ) )
        = e4 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e3 )
      | ( ( e5 @ ( e5 @ op ) )
        = e3 )
      | ( ( e5 @ ( e4 @ op ) )
        = e3 )
      | ( ( e5 @ ( e3 @ op ) )
        = e3 )
      | ( ( e5 @ ( e2 @ op ) )
        = e3 )
      | ( ( e5 @ ( e1 @ op ) )
        = e3 )
      | ( ( e5 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e3 )
      | ( ( e5 @ ( e5 @ op ) )
        = e3 )
      | ( ( e4 @ ( e5 @ op ) )
        = e3 )
      | ( ( e3 @ ( e5 @ op ) )
        = e3 )
      | ( ( e2 @ ( e5 @ op ) )
        = e3 )
      | ( ( e1 @ ( e5 @ op ) )
        = e3 )
      | ( ( e0 @ ( e5 @ op ) )
        = e3 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e2 )
      | ( ( e5 @ ( e5 @ op ) )
        = e2 )
      | ( ( e5 @ ( e4 @ op ) )
        = e2 )
      | ( ( e5 @ ( e3 @ op ) )
        = e2 )
      | ( ( e5 @ ( e2 @ op ) )
        = e2 )
      | ( ( e5 @ ( e1 @ op ) )
        = e2 )
      | ( ( e5 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e2 )
      | ( ( e5 @ ( e5 @ op ) )
        = e2 )
      | ( ( e4 @ ( e5 @ op ) )
        = e2 )
      | ( ( e3 @ ( e5 @ op ) )
        = e2 )
      | ( ( e2 @ ( e5 @ op ) )
        = e2 )
      | ( ( e1 @ ( e5 @ op ) )
        = e2 )
      | ( ( e0 @ ( e5 @ op ) )
        = e2 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e1 )
      | ( ( e5 @ ( e5 @ op ) )
        = e1 )
      | ( ( e5 @ ( e4 @ op ) )
        = e1 )
      | ( ( e5 @ ( e3 @ op ) )
        = e1 )
      | ( ( e5 @ ( e2 @ op ) )
        = e1 )
      | ( ( e5 @ ( e1 @ op ) )
        = e1 )
      | ( ( e5 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e1 )
      | ( ( e5 @ ( e5 @ op ) )
        = e1 )
      | ( ( e4 @ ( e5 @ op ) )
        = e1 )
      | ( ( e3 @ ( e5 @ op ) )
        = e1 )
      | ( ( e2 @ ( e5 @ op ) )
        = e1 )
      | ( ( e1 @ ( e5 @ op ) )
        = e1 )
      | ( ( e0 @ ( e5 @ op ) )
        = e1 ) )
    & ( ( ( e5 @ ( e6 @ op ) )
        = e0 )
      | ( ( e5 @ ( e5 @ op ) )
        = e0 )
      | ( ( e5 @ ( e4 @ op ) )
        = e0 )
      | ( ( e5 @ ( e3 @ op ) )
        = e0 )
      | ( ( e5 @ ( e2 @ op ) )
        = e0 )
      | ( ( e5 @ ( e1 @ op ) )
        = e0 )
      | ( ( e5 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e5 @ op ) )
        = e0 )
      | ( ( e5 @ ( e5 @ op ) )
        = e0 )
      | ( ( e4 @ ( e5 @ op ) )
        = e0 )
      | ( ( e3 @ ( e5 @ op ) )
        = e0 )
      | ( ( e2 @ ( e5 @ op ) )
        = e0 )
      | ( ( e1 @ ( e5 @ op ) )
        = e0 )
      | ( ( e0 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e6 )
      | ( ( e4 @ ( e5 @ op ) )
        = e6 )
      | ( ( e4 @ ( e4 @ op ) )
        = e6 )
      | ( ( e4 @ ( e3 @ op ) )
        = e6 )
      | ( ( e4 @ ( e2 @ op ) )
        = e6 )
      | ( ( e4 @ ( e1 @ op ) )
        = e6 )
      | ( ( e4 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e6 )
      | ( ( e5 @ ( e4 @ op ) )
        = e6 )
      | ( ( e4 @ ( e4 @ op ) )
        = e6 )
      | ( ( e3 @ ( e4 @ op ) )
        = e6 )
      | ( ( e2 @ ( e4 @ op ) )
        = e6 )
      | ( ( e1 @ ( e4 @ op ) )
        = e6 )
      | ( ( e0 @ ( e4 @ op ) )
        = e6 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e5 )
      | ( ( e4 @ ( e5 @ op ) )
        = e5 )
      | ( ( e4 @ ( e4 @ op ) )
        = e5 )
      | ( ( e4 @ ( e3 @ op ) )
        = e5 )
      | ( ( e4 @ ( e2 @ op ) )
        = e5 )
      | ( ( e4 @ ( e1 @ op ) )
        = e5 )
      | ( ( e4 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e5 )
      | ( ( e5 @ ( e4 @ op ) )
        = e5 )
      | ( ( e4 @ ( e4 @ op ) )
        = e5 )
      | ( ( e3 @ ( e4 @ op ) )
        = e5 )
      | ( ( e2 @ ( e4 @ op ) )
        = e5 )
      | ( ( e1 @ ( e4 @ op ) )
        = e5 )
      | ( ( e0 @ ( e4 @ op ) )
        = e5 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e4 )
      | ( ( e4 @ ( e5 @ op ) )
        = e4 )
      | ( ( e4 @ ( e4 @ op ) )
        = e4 )
      | ( ( e4 @ ( e3 @ op ) )
        = e4 )
      | ( ( e4 @ ( e2 @ op ) )
        = e4 )
      | ( ( e4 @ ( e1 @ op ) )
        = e4 )
      | ( ( e4 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e4 )
      | ( ( e5 @ ( e4 @ op ) )
        = e4 )
      | ( ( e4 @ ( e4 @ op ) )
        = e4 )
      | ( ( e3 @ ( e4 @ op ) )
        = e4 )
      | ( ( e2 @ ( e4 @ op ) )
        = e4 )
      | ( ( e1 @ ( e4 @ op ) )
        = e4 )
      | ( ( e0 @ ( e4 @ op ) )
        = e4 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e3 )
      | ( ( e4 @ ( e5 @ op ) )
        = e3 )
      | ( ( e4 @ ( e4 @ op ) )
        = e3 )
      | ( ( e4 @ ( e3 @ op ) )
        = e3 )
      | ( ( e4 @ ( e2 @ op ) )
        = e3 )
      | ( ( e4 @ ( e1 @ op ) )
        = e3 )
      | ( ( e4 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e3 )
      | ( ( e5 @ ( e4 @ op ) )
        = e3 )
      | ( ( e4 @ ( e4 @ op ) )
        = e3 )
      | ( ( e3 @ ( e4 @ op ) )
        = e3 )
      | ( ( e2 @ ( e4 @ op ) )
        = e3 )
      | ( ( e1 @ ( e4 @ op ) )
        = e3 )
      | ( ( e0 @ ( e4 @ op ) )
        = e3 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e2 )
      | ( ( e4 @ ( e5 @ op ) )
        = e2 )
      | ( ( e4 @ ( e4 @ op ) )
        = e2 )
      | ( ( e4 @ ( e3 @ op ) )
        = e2 )
      | ( ( e4 @ ( e2 @ op ) )
        = e2 )
      | ( ( e4 @ ( e1 @ op ) )
        = e2 )
      | ( ( e4 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e2 )
      | ( ( e5 @ ( e4 @ op ) )
        = e2 )
      | ( ( e4 @ ( e4 @ op ) )
        = e2 )
      | ( ( e3 @ ( e4 @ op ) )
        = e2 )
      | ( ( e2 @ ( e4 @ op ) )
        = e2 )
      | ( ( e1 @ ( e4 @ op ) )
        = e2 )
      | ( ( e0 @ ( e4 @ op ) )
        = e2 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e1 )
      | ( ( e4 @ ( e5 @ op ) )
        = e1 )
      | ( ( e4 @ ( e4 @ op ) )
        = e1 )
      | ( ( e4 @ ( e3 @ op ) )
        = e1 )
      | ( ( e4 @ ( e2 @ op ) )
        = e1 )
      | ( ( e4 @ ( e1 @ op ) )
        = e1 )
      | ( ( e4 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e1 )
      | ( ( e5 @ ( e4 @ op ) )
        = e1 )
      | ( ( e4 @ ( e4 @ op ) )
        = e1 )
      | ( ( e3 @ ( e4 @ op ) )
        = e1 )
      | ( ( e2 @ ( e4 @ op ) )
        = e1 )
      | ( ( e1 @ ( e4 @ op ) )
        = e1 )
      | ( ( e0 @ ( e4 @ op ) )
        = e1 ) )
    & ( ( ( e4 @ ( e6 @ op ) )
        = e0 )
      | ( ( e4 @ ( e5 @ op ) )
        = e0 )
      | ( ( e4 @ ( e4 @ op ) )
        = e0 )
      | ( ( e4 @ ( e3 @ op ) )
        = e0 )
      | ( ( e4 @ ( e2 @ op ) )
        = e0 )
      | ( ( e4 @ ( e1 @ op ) )
        = e0 )
      | ( ( e4 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e4 @ op ) )
        = e0 )
      | ( ( e5 @ ( e4 @ op ) )
        = e0 )
      | ( ( e4 @ ( e4 @ op ) )
        = e0 )
      | ( ( e3 @ ( e4 @ op ) )
        = e0 )
      | ( ( e2 @ ( e4 @ op ) )
        = e0 )
      | ( ( e1 @ ( e4 @ op ) )
        = e0 )
      | ( ( e0 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e6 )
      | ( ( e3 @ ( e5 @ op ) )
        = e6 )
      | ( ( e3 @ ( e4 @ op ) )
        = e6 )
      | ( ( e3 @ ( e3 @ op ) )
        = e6 )
      | ( ( e3 @ ( e2 @ op ) )
        = e6 )
      | ( ( e3 @ ( e1 @ op ) )
        = e6 )
      | ( ( e3 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e6 )
      | ( ( e5 @ ( e3 @ op ) )
        = e6 )
      | ( ( e4 @ ( e3 @ op ) )
        = e6 )
      | ( ( e3 @ ( e3 @ op ) )
        = e6 )
      | ( ( e2 @ ( e3 @ op ) )
        = e6 )
      | ( ( e1 @ ( e3 @ op ) )
        = e6 )
      | ( ( e0 @ ( e3 @ op ) )
        = e6 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e5 )
      | ( ( e3 @ ( e5 @ op ) )
        = e5 )
      | ( ( e3 @ ( e4 @ op ) )
        = e5 )
      | ( ( e3 @ ( e3 @ op ) )
        = e5 )
      | ( ( e3 @ ( e2 @ op ) )
        = e5 )
      | ( ( e3 @ ( e1 @ op ) )
        = e5 )
      | ( ( e3 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e5 )
      | ( ( e5 @ ( e3 @ op ) )
        = e5 )
      | ( ( e4 @ ( e3 @ op ) )
        = e5 )
      | ( ( e3 @ ( e3 @ op ) )
        = e5 )
      | ( ( e2 @ ( e3 @ op ) )
        = e5 )
      | ( ( e1 @ ( e3 @ op ) )
        = e5 )
      | ( ( e0 @ ( e3 @ op ) )
        = e5 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e4 )
      | ( ( e3 @ ( e5 @ op ) )
        = e4 )
      | ( ( e3 @ ( e4 @ op ) )
        = e4 )
      | ( ( e3 @ ( e3 @ op ) )
        = e4 )
      | ( ( e3 @ ( e2 @ op ) )
        = e4 )
      | ( ( e3 @ ( e1 @ op ) )
        = e4 )
      | ( ( e3 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e4 )
      | ( ( e5 @ ( e3 @ op ) )
        = e4 )
      | ( ( e4 @ ( e3 @ op ) )
        = e4 )
      | ( ( e3 @ ( e3 @ op ) )
        = e4 )
      | ( ( e2 @ ( e3 @ op ) )
        = e4 )
      | ( ( e1 @ ( e3 @ op ) )
        = e4 )
      | ( ( e0 @ ( e3 @ op ) )
        = e4 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e3 )
      | ( ( e3 @ ( e5 @ op ) )
        = e3 )
      | ( ( e3 @ ( e4 @ op ) )
        = e3 )
      | ( ( e3 @ ( e3 @ op ) )
        = e3 )
      | ( ( e3 @ ( e2 @ op ) )
        = e3 )
      | ( ( e3 @ ( e1 @ op ) )
        = e3 )
      | ( ( e3 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e3 )
      | ( ( e5 @ ( e3 @ op ) )
        = e3 )
      | ( ( e4 @ ( e3 @ op ) )
        = e3 )
      | ( ( e3 @ ( e3 @ op ) )
        = e3 )
      | ( ( e2 @ ( e3 @ op ) )
        = e3 )
      | ( ( e1 @ ( e3 @ op ) )
        = e3 )
      | ( ( e0 @ ( e3 @ op ) )
        = e3 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e2 )
      | ( ( e3 @ ( e5 @ op ) )
        = e2 )
      | ( ( e3 @ ( e4 @ op ) )
        = e2 )
      | ( ( e3 @ ( e3 @ op ) )
        = e2 )
      | ( ( e3 @ ( e2 @ op ) )
        = e2 )
      | ( ( e3 @ ( e1 @ op ) )
        = e2 )
      | ( ( e3 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e2 )
      | ( ( e5 @ ( e3 @ op ) )
        = e2 )
      | ( ( e4 @ ( e3 @ op ) )
        = e2 )
      | ( ( e3 @ ( e3 @ op ) )
        = e2 )
      | ( ( e2 @ ( e3 @ op ) )
        = e2 )
      | ( ( e1 @ ( e3 @ op ) )
        = e2 )
      | ( ( e0 @ ( e3 @ op ) )
        = e2 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e1 )
      | ( ( e3 @ ( e5 @ op ) )
        = e1 )
      | ( ( e3 @ ( e4 @ op ) )
        = e1 )
      | ( ( e3 @ ( e3 @ op ) )
        = e1 )
      | ( ( e3 @ ( e2 @ op ) )
        = e1 )
      | ( ( e3 @ ( e1 @ op ) )
        = e1 )
      | ( ( e3 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e1 )
      | ( ( e5 @ ( e3 @ op ) )
        = e1 )
      | ( ( e4 @ ( e3 @ op ) )
        = e1 )
      | ( ( e3 @ ( e3 @ op ) )
        = e1 )
      | ( ( e2 @ ( e3 @ op ) )
        = e1 )
      | ( ( e1 @ ( e3 @ op ) )
        = e1 )
      | ( ( e0 @ ( e3 @ op ) )
        = e1 ) )
    & ( ( ( e3 @ ( e6 @ op ) )
        = e0 )
      | ( ( e3 @ ( e5 @ op ) )
        = e0 )
      | ( ( e3 @ ( e4 @ op ) )
        = e0 )
      | ( ( e3 @ ( e3 @ op ) )
        = e0 )
      | ( ( e3 @ ( e2 @ op ) )
        = e0 )
      | ( ( e3 @ ( e1 @ op ) )
        = e0 )
      | ( ( e3 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e3 @ op ) )
        = e0 )
      | ( ( e5 @ ( e3 @ op ) )
        = e0 )
      | ( ( e4 @ ( e3 @ op ) )
        = e0 )
      | ( ( e3 @ ( e3 @ op ) )
        = e0 )
      | ( ( e2 @ ( e3 @ op ) )
        = e0 )
      | ( ( e1 @ ( e3 @ op ) )
        = e0 )
      | ( ( e0 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e6 )
      | ( ( e2 @ ( e5 @ op ) )
        = e6 )
      | ( ( e2 @ ( e4 @ op ) )
        = e6 )
      | ( ( e2 @ ( e3 @ op ) )
        = e6 )
      | ( ( e2 @ ( e2 @ op ) )
        = e6 )
      | ( ( e2 @ ( e1 @ op ) )
        = e6 )
      | ( ( e2 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e6 )
      | ( ( e5 @ ( e2 @ op ) )
        = e6 )
      | ( ( e4 @ ( e2 @ op ) )
        = e6 )
      | ( ( e3 @ ( e2 @ op ) )
        = e6 )
      | ( ( e2 @ ( e2 @ op ) )
        = e6 )
      | ( ( e1 @ ( e2 @ op ) )
        = e6 )
      | ( ( e0 @ ( e2 @ op ) )
        = e6 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e5 )
      | ( ( e2 @ ( e5 @ op ) )
        = e5 )
      | ( ( e2 @ ( e4 @ op ) )
        = e5 )
      | ( ( e2 @ ( e3 @ op ) )
        = e5 )
      | ( ( e2 @ ( e2 @ op ) )
        = e5 )
      | ( ( e2 @ ( e1 @ op ) )
        = e5 )
      | ( ( e2 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e5 )
      | ( ( e5 @ ( e2 @ op ) )
        = e5 )
      | ( ( e4 @ ( e2 @ op ) )
        = e5 )
      | ( ( e3 @ ( e2 @ op ) )
        = e5 )
      | ( ( e2 @ ( e2 @ op ) )
        = e5 )
      | ( ( e1 @ ( e2 @ op ) )
        = e5 )
      | ( ( e0 @ ( e2 @ op ) )
        = e5 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e4 )
      | ( ( e2 @ ( e5 @ op ) )
        = e4 )
      | ( ( e2 @ ( e4 @ op ) )
        = e4 )
      | ( ( e2 @ ( e3 @ op ) )
        = e4 )
      | ( ( e2 @ ( e2 @ op ) )
        = e4 )
      | ( ( e2 @ ( e1 @ op ) )
        = e4 )
      | ( ( e2 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e4 )
      | ( ( e5 @ ( e2 @ op ) )
        = e4 )
      | ( ( e4 @ ( e2 @ op ) )
        = e4 )
      | ( ( e3 @ ( e2 @ op ) )
        = e4 )
      | ( ( e2 @ ( e2 @ op ) )
        = e4 )
      | ( ( e1 @ ( e2 @ op ) )
        = e4 )
      | ( ( e0 @ ( e2 @ op ) )
        = e4 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e3 )
      | ( ( e2 @ ( e5 @ op ) )
        = e3 )
      | ( ( e2 @ ( e4 @ op ) )
        = e3 )
      | ( ( e2 @ ( e3 @ op ) )
        = e3 )
      | ( ( e2 @ ( e2 @ op ) )
        = e3 )
      | ( ( e2 @ ( e1 @ op ) )
        = e3 )
      | ( ( e2 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e3 )
      | ( ( e5 @ ( e2 @ op ) )
        = e3 )
      | ( ( e4 @ ( e2 @ op ) )
        = e3 )
      | ( ( e3 @ ( e2 @ op ) )
        = e3 )
      | ( ( e2 @ ( e2 @ op ) )
        = e3 )
      | ( ( e1 @ ( e2 @ op ) )
        = e3 )
      | ( ( e0 @ ( e2 @ op ) )
        = e3 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e2 )
      | ( ( e2 @ ( e5 @ op ) )
        = e2 )
      | ( ( e2 @ ( e4 @ op ) )
        = e2 )
      | ( ( e2 @ ( e3 @ op ) )
        = e2 )
      | ( ( e2 @ ( e2 @ op ) )
        = e2 )
      | ( ( e2 @ ( e1 @ op ) )
        = e2 )
      | ( ( e2 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e2 )
      | ( ( e5 @ ( e2 @ op ) )
        = e2 )
      | ( ( e4 @ ( e2 @ op ) )
        = e2 )
      | ( ( e3 @ ( e2 @ op ) )
        = e2 )
      | ( ( e2 @ ( e2 @ op ) )
        = e2 )
      | ( ( e1 @ ( e2 @ op ) )
        = e2 )
      | ( ( e0 @ ( e2 @ op ) )
        = e2 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e1 )
      | ( ( e2 @ ( e5 @ op ) )
        = e1 )
      | ( ( e2 @ ( e4 @ op ) )
        = e1 )
      | ( ( e2 @ ( e3 @ op ) )
        = e1 )
      | ( ( e2 @ ( e2 @ op ) )
        = e1 )
      | ( ( e2 @ ( e1 @ op ) )
        = e1 )
      | ( ( e2 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e1 )
      | ( ( e5 @ ( e2 @ op ) )
        = e1 )
      | ( ( e4 @ ( e2 @ op ) )
        = e1 )
      | ( ( e3 @ ( e2 @ op ) )
        = e1 )
      | ( ( e2 @ ( e2 @ op ) )
        = e1 )
      | ( ( e1 @ ( e2 @ op ) )
        = e1 )
      | ( ( e0 @ ( e2 @ op ) )
        = e1 ) )
    & ( ( ( e2 @ ( e6 @ op ) )
        = e0 )
      | ( ( e2 @ ( e5 @ op ) )
        = e0 )
      | ( ( e2 @ ( e4 @ op ) )
        = e0 )
      | ( ( e2 @ ( e3 @ op ) )
        = e0 )
      | ( ( e2 @ ( e2 @ op ) )
        = e0 )
      | ( ( e2 @ ( e1 @ op ) )
        = e0 )
      | ( ( e2 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e2 @ op ) )
        = e0 )
      | ( ( e5 @ ( e2 @ op ) )
        = e0 )
      | ( ( e4 @ ( e2 @ op ) )
        = e0 )
      | ( ( e3 @ ( e2 @ op ) )
        = e0 )
      | ( ( e2 @ ( e2 @ op ) )
        = e0 )
      | ( ( e1 @ ( e2 @ op ) )
        = e0 )
      | ( ( e0 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e6 )
      | ( ( e1 @ ( e5 @ op ) )
        = e6 )
      | ( ( e1 @ ( e4 @ op ) )
        = e6 )
      | ( ( e1 @ ( e3 @ op ) )
        = e6 )
      | ( ( e1 @ ( e2 @ op ) )
        = e6 )
      | ( ( e1 @ ( e1 @ op ) )
        = e6 )
      | ( ( e1 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e6 )
      | ( ( e5 @ ( e1 @ op ) )
        = e6 )
      | ( ( e4 @ ( e1 @ op ) )
        = e6 )
      | ( ( e3 @ ( e1 @ op ) )
        = e6 )
      | ( ( e2 @ ( e1 @ op ) )
        = e6 )
      | ( ( e1 @ ( e1 @ op ) )
        = e6 )
      | ( ( e0 @ ( e1 @ op ) )
        = e6 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e5 )
      | ( ( e1 @ ( e5 @ op ) )
        = e5 )
      | ( ( e1 @ ( e4 @ op ) )
        = e5 )
      | ( ( e1 @ ( e3 @ op ) )
        = e5 )
      | ( ( e1 @ ( e2 @ op ) )
        = e5 )
      | ( ( e1 @ ( e1 @ op ) )
        = e5 )
      | ( ( e1 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e5 )
      | ( ( e5 @ ( e1 @ op ) )
        = e5 )
      | ( ( e4 @ ( e1 @ op ) )
        = e5 )
      | ( ( e3 @ ( e1 @ op ) )
        = e5 )
      | ( ( e2 @ ( e1 @ op ) )
        = e5 )
      | ( ( e1 @ ( e1 @ op ) )
        = e5 )
      | ( ( e0 @ ( e1 @ op ) )
        = e5 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e4 )
      | ( ( e1 @ ( e5 @ op ) )
        = e4 )
      | ( ( e1 @ ( e4 @ op ) )
        = e4 )
      | ( ( e1 @ ( e3 @ op ) )
        = e4 )
      | ( ( e1 @ ( e2 @ op ) )
        = e4 )
      | ( ( e1 @ ( e1 @ op ) )
        = e4 )
      | ( ( e1 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e4 )
      | ( ( e5 @ ( e1 @ op ) )
        = e4 )
      | ( ( e4 @ ( e1 @ op ) )
        = e4 )
      | ( ( e3 @ ( e1 @ op ) )
        = e4 )
      | ( ( e2 @ ( e1 @ op ) )
        = e4 )
      | ( ( e1 @ ( e1 @ op ) )
        = e4 )
      | ( ( e0 @ ( e1 @ op ) )
        = e4 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e3 )
      | ( ( e1 @ ( e5 @ op ) )
        = e3 )
      | ( ( e1 @ ( e4 @ op ) )
        = e3 )
      | ( ( e1 @ ( e3 @ op ) )
        = e3 )
      | ( ( e1 @ ( e2 @ op ) )
        = e3 )
      | ( ( e1 @ ( e1 @ op ) )
        = e3 )
      | ( ( e1 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e3 )
      | ( ( e5 @ ( e1 @ op ) )
        = e3 )
      | ( ( e4 @ ( e1 @ op ) )
        = e3 )
      | ( ( e3 @ ( e1 @ op ) )
        = e3 )
      | ( ( e2 @ ( e1 @ op ) )
        = e3 )
      | ( ( e1 @ ( e1 @ op ) )
        = e3 )
      | ( ( e0 @ ( e1 @ op ) )
        = e3 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e2 )
      | ( ( e1 @ ( e5 @ op ) )
        = e2 )
      | ( ( e1 @ ( e4 @ op ) )
        = e2 )
      | ( ( e1 @ ( e3 @ op ) )
        = e2 )
      | ( ( e1 @ ( e2 @ op ) )
        = e2 )
      | ( ( e1 @ ( e1 @ op ) )
        = e2 )
      | ( ( e1 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e2 )
      | ( ( e5 @ ( e1 @ op ) )
        = e2 )
      | ( ( e4 @ ( e1 @ op ) )
        = e2 )
      | ( ( e3 @ ( e1 @ op ) )
        = e2 )
      | ( ( e2 @ ( e1 @ op ) )
        = e2 )
      | ( ( e1 @ ( e1 @ op ) )
        = e2 )
      | ( ( e0 @ ( e1 @ op ) )
        = e2 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e1 )
      | ( ( e1 @ ( e5 @ op ) )
        = e1 )
      | ( ( e1 @ ( e4 @ op ) )
        = e1 )
      | ( ( e1 @ ( e3 @ op ) )
        = e1 )
      | ( ( e1 @ ( e2 @ op ) )
        = e1 )
      | ( ( e1 @ ( e1 @ op ) )
        = e1 )
      | ( ( e1 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e1 )
      | ( ( e5 @ ( e1 @ op ) )
        = e1 )
      | ( ( e4 @ ( e1 @ op ) )
        = e1 )
      | ( ( e3 @ ( e1 @ op ) )
        = e1 )
      | ( ( e2 @ ( e1 @ op ) )
        = e1 )
      | ( ( e1 @ ( e1 @ op ) )
        = e1 )
      | ( ( e0 @ ( e1 @ op ) )
        = e1 ) )
    & ( ( ( e1 @ ( e6 @ op ) )
        = e0 )
      | ( ( e1 @ ( e5 @ op ) )
        = e0 )
      | ( ( e1 @ ( e4 @ op ) )
        = e0 )
      | ( ( e1 @ ( e3 @ op ) )
        = e0 )
      | ( ( e1 @ ( e2 @ op ) )
        = e0 )
      | ( ( e1 @ ( e1 @ op ) )
        = e0 )
      | ( ( e1 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e1 @ op ) )
        = e0 )
      | ( ( e5 @ ( e1 @ op ) )
        = e0 )
      | ( ( e4 @ ( e1 @ op ) )
        = e0 )
      | ( ( e3 @ ( e1 @ op ) )
        = e0 )
      | ( ( e2 @ ( e1 @ op ) )
        = e0 )
      | ( ( e1 @ ( e1 @ op ) )
        = e0 )
      | ( ( e0 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e6 )
      | ( ( e0 @ ( e5 @ op ) )
        = e6 )
      | ( ( e0 @ ( e4 @ op ) )
        = e6 )
      | ( ( e0 @ ( e3 @ op ) )
        = e6 )
      | ( ( e0 @ ( e2 @ op ) )
        = e6 )
      | ( ( e0 @ ( e1 @ op ) )
        = e6 )
      | ( ( e0 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e6 )
      | ( ( e5 @ ( e0 @ op ) )
        = e6 )
      | ( ( e4 @ ( e0 @ op ) )
        = e6 )
      | ( ( e3 @ ( e0 @ op ) )
        = e6 )
      | ( ( e2 @ ( e0 @ op ) )
        = e6 )
      | ( ( e1 @ ( e0 @ op ) )
        = e6 )
      | ( ( e0 @ ( e0 @ op ) )
        = e6 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e5 )
      | ( ( e0 @ ( e5 @ op ) )
        = e5 )
      | ( ( e0 @ ( e4 @ op ) )
        = e5 )
      | ( ( e0 @ ( e3 @ op ) )
        = e5 )
      | ( ( e0 @ ( e2 @ op ) )
        = e5 )
      | ( ( e0 @ ( e1 @ op ) )
        = e5 )
      | ( ( e0 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e5 )
      | ( ( e5 @ ( e0 @ op ) )
        = e5 )
      | ( ( e4 @ ( e0 @ op ) )
        = e5 )
      | ( ( e3 @ ( e0 @ op ) )
        = e5 )
      | ( ( e2 @ ( e0 @ op ) )
        = e5 )
      | ( ( e1 @ ( e0 @ op ) )
        = e5 )
      | ( ( e0 @ ( e0 @ op ) )
        = e5 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e4 )
      | ( ( e0 @ ( e5 @ op ) )
        = e4 )
      | ( ( e0 @ ( e4 @ op ) )
        = e4 )
      | ( ( e0 @ ( e3 @ op ) )
        = e4 )
      | ( ( e0 @ ( e2 @ op ) )
        = e4 )
      | ( ( e0 @ ( e1 @ op ) )
        = e4 )
      | ( ( e0 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e4 )
      | ( ( e5 @ ( e0 @ op ) )
        = e4 )
      | ( ( e4 @ ( e0 @ op ) )
        = e4 )
      | ( ( e3 @ ( e0 @ op ) )
        = e4 )
      | ( ( e2 @ ( e0 @ op ) )
        = e4 )
      | ( ( e1 @ ( e0 @ op ) )
        = e4 )
      | ( ( e0 @ ( e0 @ op ) )
        = e4 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e3 )
      | ( ( e0 @ ( e5 @ op ) )
        = e3 )
      | ( ( e0 @ ( e4 @ op ) )
        = e3 )
      | ( ( e0 @ ( e3 @ op ) )
        = e3 )
      | ( ( e0 @ ( e2 @ op ) )
        = e3 )
      | ( ( e0 @ ( e1 @ op ) )
        = e3 )
      | ( ( e0 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e3 )
      | ( ( e5 @ ( e0 @ op ) )
        = e3 )
      | ( ( e4 @ ( e0 @ op ) )
        = e3 )
      | ( ( e3 @ ( e0 @ op ) )
        = e3 )
      | ( ( e2 @ ( e0 @ op ) )
        = e3 )
      | ( ( e1 @ ( e0 @ op ) )
        = e3 )
      | ( ( e0 @ ( e0 @ op ) )
        = e3 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e2 )
      | ( ( e0 @ ( e5 @ op ) )
        = e2 )
      | ( ( e0 @ ( e4 @ op ) )
        = e2 )
      | ( ( e0 @ ( e3 @ op ) )
        = e2 )
      | ( ( e0 @ ( e2 @ op ) )
        = e2 )
      | ( ( e0 @ ( e1 @ op ) )
        = e2 )
      | ( ( e0 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e2 )
      | ( ( e5 @ ( e0 @ op ) )
        = e2 )
      | ( ( e4 @ ( e0 @ op ) )
        = e2 )
      | ( ( e3 @ ( e0 @ op ) )
        = e2 )
      | ( ( e2 @ ( e0 @ op ) )
        = e2 )
      | ( ( e1 @ ( e0 @ op ) )
        = e2 )
      | ( ( e0 @ ( e0 @ op ) )
        = e2 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e1 )
      | ( ( e0 @ ( e5 @ op ) )
        = e1 )
      | ( ( e0 @ ( e4 @ op ) )
        = e1 )
      | ( ( e0 @ ( e3 @ op ) )
        = e1 )
      | ( ( e0 @ ( e2 @ op ) )
        = e1 )
      | ( ( e0 @ ( e1 @ op ) )
        = e1 )
      | ( ( e0 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e1 )
      | ( ( e5 @ ( e0 @ op ) )
        = e1 )
      | ( ( e4 @ ( e0 @ op ) )
        = e1 )
      | ( ( e3 @ ( e0 @ op ) )
        = e1 )
      | ( ( e2 @ ( e0 @ op ) )
        = e1 )
      | ( ( e1 @ ( e0 @ op ) )
        = e1 )
      | ( ( e0 @ ( e0 @ op ) )
        = e1 ) )
    & ( ( ( e0 @ ( e6 @ op ) )
        = e0 )
      | ( ( e0 @ ( e5 @ op ) )
        = e0 )
      | ( ( e0 @ ( e4 @ op ) )
        = e0 )
      | ( ( e0 @ ( e3 @ op ) )
        = e0 )
      | ( ( e0 @ ( e2 @ op ) )
        = e0 )
      | ( ( e0 @ ( e1 @ op ) )
        = e0 )
      | ( ( e0 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( e6 @ ( e0 @ op ) )
        = e0 )
      | ( ( e5 @ ( e0 @ op ) )
        = e0 )
      | ( ( e4 @ ( e0 @ op ) )
        = e0 )
      | ( ( e3 @ ( e0 @ op ) )
        = e0 )
      | ( ( e2 @ ( e0 @ op ) )
        = e0 )
      | ( ( e1 @ ( e0 @ op ) )
        = e0 )
      | ( ( e0 @ ( e0 @ op ) )
        = e0 ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).

thf(5,axiom,
    ( ( ( e6 @ ( e6 @ ( e6 @ ( e6 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e5 @ ( e5 @ ( e6 @ ( e5 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e4 @ ( e4 @ ( e6 @ ( e4 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e3 @ ( e3 @ ( e6 @ ( e3 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e2 @ ( e2 @ ( e6 @ ( e2 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e1 @ ( e1 @ ( e6 @ ( e1 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e0 @ ( e0 @ ( e6 @ ( e0 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e6 @ ( e6 @ ( e5 @ ( e6 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e5 @ ( e5 @ ( e5 @ ( e5 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e4 @ ( e4 @ ( e5 @ ( e4 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e3 @ ( e3 @ ( e5 @ ( e3 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e2 @ ( e2 @ ( e5 @ ( e2 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e1 @ ( e1 @ ( e5 @ ( e1 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e0 @ ( e0 @ ( e5 @ ( e0 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e6 @ ( e6 @ ( e4 @ ( e6 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e5 @ ( e5 @ ( e4 @ ( e5 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e4 @ ( e4 @ ( e4 @ ( e4 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e3 @ ( e3 @ ( e4 @ ( e3 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e2 @ ( e2 @ ( e4 @ ( e2 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e1 @ ( e1 @ ( e4 @ ( e1 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e0 @ ( e0 @ ( e4 @ ( e0 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e6 @ ( e6 @ ( e3 @ ( e6 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e5 @ ( e5 @ ( e3 @ ( e5 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e4 @ ( e4 @ ( e3 @ ( e4 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e3 @ ( e3 @ ( e3 @ ( e3 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e2 @ ( e2 @ ( e3 @ ( e2 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e1 @ ( e1 @ ( e3 @ ( e1 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e0 @ ( e0 @ ( e3 @ ( e0 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e6 @ ( e6 @ ( e2 @ ( e6 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e5 @ ( e5 @ ( e2 @ ( e5 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e4 @ ( e4 @ ( e2 @ ( e4 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e3 @ ( e3 @ ( e2 @ ( e3 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e2 @ ( e2 @ ( e2 @ ( e2 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e1 @ ( e1 @ ( e2 @ ( e1 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e0 @ ( e0 @ ( e2 @ ( e0 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e6 @ ( e6 @ ( e1 @ ( e6 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e5 @ ( e5 @ ( e1 @ ( e5 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e4 @ ( e4 @ ( e1 @ ( e4 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e3 @ ( e3 @ ( e1 @ ( e3 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e2 @ ( e2 @ ( e1 @ ( e2 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e1 @ ( e1 @ ( e1 @ ( e1 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e0 @ ( e0 @ ( e1 @ ( e0 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e6 @ ( e6 @ ( e0 @ ( e6 @ op ) @ op ) @ op ) )
      = e0 )
    & ( ( e5 @ ( e5 @ ( e0 @ ( e5 @ op ) @ op ) @ op ) )
      = e0 )
    & ( ( e4 @ ( e4 @ ( e0 @ ( e4 @ op ) @ op ) @ op ) )
      = e0 )
    & ( ( e3 @ ( e3 @ ( e0 @ ( e3 @ op ) @ op ) @ op ) )
      = e0 )
    & ( ( e2 @ ( e2 @ ( e0 @ ( e2 @ op ) @ op ) @ op ) )
      = e0 )
    & ( ( e1 @ ( e1 @ ( e0 @ ( e1 @ op ) @ op ) @ op ) )
      = e0 )
    & ( ( e0 @ ( e0 @ ( e0 @ ( e0 @ op ) @ op ) @ op ) )
      = e0 ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).

thf(340,plain,
    ( ( ( e6 @ ( e6 @ ( e6 @ ( e6 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e5 @ ( e5 @ ( e6 @ ( e5 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e4 @ ( e4 @ ( e6 @ ( e4 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e3 @ ( e3 @ ( e6 @ ( e3 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e2 @ ( e2 @ ( e6 @ ( e2 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e1 @ ( e1 @ ( e6 @ ( e1 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e0 @ ( e0 @ ( e6 @ ( e0 @ op ) @ op ) @ op ) )
      = e6 )
    & ( ( e6 @ ( e6 @ ( e5 @ ( e6 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e5 @ ( e5 @ ( e5 @ ( e5 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e4 @ ( e4 @ ( e5 @ ( e4 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e3 @ ( e3 @ ( e5 @ ( e3 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e2 @ ( e2 @ ( e5 @ ( e2 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e1 @ ( e1 @ ( e5 @ ( e1 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e0 @ ( e0 @ ( e5 @ ( e0 @ op ) @ op ) @ op ) )
      = e5 )
    & ( ( e6 @ ( e6 @ ( e4 @ ( e6 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e5 @ ( e5 @ ( e4 @ ( e5 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e4 @ ( e4 @ ( e4 @ ( e4 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e3 @ ( e3 @ ( e4 @ ( e3 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e2 @ ( e2 @ ( e4 @ ( e2 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e1 @ ( e1 @ ( e4 @ ( e1 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e0 @ ( e0 @ ( e4 @ ( e0 @ op ) @ op ) @ op ) )
      = e4 )
    & ( ( e6 @ ( e6 @ ( e3 @ ( e6 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e5 @ ( e5 @ ( e3 @ ( e5 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e4 @ ( e4 @ ( e3 @ ( e4 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e3 @ ( e3 @ ( e3 @ ( e3 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e2 @ ( e2 @ ( e3 @ ( e2 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e1 @ ( e1 @ ( e3 @ ( e1 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e0 @ ( e0 @ ( e3 @ ( e0 @ op ) @ op ) @ op ) )
      = e3 )
    & ( ( e6 @ ( e6 @ ( e2 @ ( e6 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e5 @ ( e5 @ ( e2 @ ( e5 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e4 @ ( e4 @ ( e2 @ ( e4 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e3 @ ( e3 @ ( e2 @ ( e3 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e2 @ ( e2 @ ( e2 @ ( e2 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e1 @ ( e1 @ ( e2 @ ( e1 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e0 @ ( e0 @ ( e2 @ ( e0 @ op ) @ op ) @ op ) )
      = e2 )
    & ( ( e6 @ ( e6 @ ( e1 @ ( e6 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e5 @ ( e5 @ ( e1 @ ( e5 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e4 @ ( e4 @ ( e1 @ ( e4 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e3 @ ( e3 @ ( e1 @ ( e3 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e2 @ ( e2 @ ( e1 @ ( e2 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e1 @ ( e1 @ ( e1 @ ( e1 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e0 @ ( e0 @ ( e1 @ ( e0 @ op ) @ op ) @ op ) )
      = e1 )
    & ( ( e6 @ ( e6 @ ( e0 @ ( e6 @ op ) @ op ) @ op ) )
      = e0 )
    & ( ( e5 @ ( e5 @ ( e0 @ ( e5 @ op ) @ op ) @ op ) )
      = e0 )
    & ( ( e4 @ ( e4 @ ( e0 @ ( e4 @ op ) @ op ) @ op ) )
      = e0 )
    & ( ( e3 @ ( e3 @ ( e0 @ ( e3 @ op ) @ op ) @ op ) )
      = e0 )
    & ( ( e2 @ ( e2 @ ( e0 @ ( e2 @ op ) @ op ) @ op ) )
      = e0 )
    & ( ( e1 @ ( e1 @ ( e0 @ ( e1 @ op ) @ op ) @ op ) )
      = e0 )
    & ( ( e0 @ ( e0 @ ( e0 @ ( e0 @ op ) @ op ) @ op ) )
      = e0 ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).

thf(1,conjecture,
    ( ( ( ( ( e6 @ ( e6 @ op ) )
         != e6 )
        | ( ( e5 @ ( e5 @ op ) )
         != e5 )
        | ( ( e4 @ ( e4 @ op ) )
         != e4 )
        | ( ( e3 @ ( e3 @ op ) )
         != e3 )
        | ( ( e2 @ ( e2 @ op ) )
         != e2 )
        | ( ( e1 @ ( e1 @ op ) )
         != e1 )
        | ( ( e0 @ ( e0 @ op ) )
         != e0 ) )
      & ( ( ( e6 @ ( e6 @ op ) )
          = e6 )
        | ( ( e5 @ ( e5 @ op ) )
          = e5 )
        | ( ( e4 @ ( e4 @ op ) )
          = e4 )
        | ( ( e3 @ ( e3 @ op ) )
          = e3 )
        | ( ( e2 @ ( e2 @ op ) )
          = e2 )
        | ( ( e1 @ ( e1 @ op ) )
          = e1 )
        | ( ( e0 @ ( e0 @ op ) )
          = e0 ) ) )
    | ( ( ( e6 @ ( e6 @ op ) )
        = e6 )
      & ( ( e5 @ ( e5 @ op ) )
        = e5 )
      & ( ( e4 @ ( e4 @ op ) )
        = e4 )
      & ( ( e3 @ ( e3 @ op ) )
        = e3 )
      & ( ( e2 @ ( e2 @ op ) )
        = e2 )
      & ( ( e1 @ ( e1 @ op ) )
        = e1 )
      & ( ( e0 @ ( e0 @ op ) )
        = e0 ) )
    | ( ( ( e6 @ ( e6 @ op ) )
       != e6 )
      & ( ( e5 @ ( e5 @ op ) )
       != e5 )
      & ( ( e4 @ ( e4 @ op ) )
       != e4 )
      & ( ( e3 @ ( e3 @ op ) )
       != e3 )
      & ( ( e2 @ ( e2 @ op ) )
       != e2 )
      & ( ( e1 @ ( e1 @ op ) )
       != e1 )
      & ( ( e0 @ ( e0 @ op ) )
       != e0 ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).

thf(2,negated_conjecture,
    ~ ( ( ( ( ( e6 @ ( e6 @ op ) )
           != e6 )
          | ( ( e5 @ ( e5 @ op ) )
           != e5 )
          | ( ( e4 @ ( e4 @ op ) )
           != e4 )
          | ( ( e3 @ ( e3 @ op ) )
           != e3 )
          | ( ( e2 @ ( e2 @ op ) )
           != e2 )
          | ( ( e1 @ ( e1 @ op ) )
           != e1 )
          | ( ( e0 @ ( e0 @ op ) )
           != e0 ) )
        & ( ( ( e6 @ ( e6 @ op ) )
            = e6 )
          | ( ( e5 @ ( e5 @ op ) )
            = e5 )
          | ( ( e4 @ ( e4 @ op ) )
            = e4 )
          | ( ( e3 @ ( e3 @ op ) )
            = e3 )
          | ( ( e2 @ ( e2 @ op ) )
            = e2 )
          | ( ( e1 @ ( e1 @ op ) )
            = e1 )
          | ( ( e0 @ ( e0 @ op ) )
            = e0 ) ) )
      | ( ( ( e6 @ ( e6 @ op ) )
          = e6 )
        & ( ( e5 @ ( e5 @ op ) )
          = e5 )
        & ( ( e4 @ ( e4 @ op ) )
          = e4 )
        & ( ( e3 @ ( e3 @ op ) )
          = e3 )
        & ( ( e2 @ ( e2 @ op ) )
          = e2 )
        & ( ( e1 @ ( e1 @ op ) )
          = e1 )
        & ( ( e0 @ ( e0 @ op ) )
          = e0 ) )
      | ( ( ( e6 @ ( e6 @ op ) )
         != e6 )
        & ( ( e5 @ ( e5 @ op ) )
         != e5 )
        & ( ( e4 @ ( e4 @ op ) )
         != e4 )
        & ( ( e3 @ ( e3 @ op ) )
         != e3 )
        & ( ( e2 @ ( e2 @ op ) )
         != e2 )
        & ( ( e1 @ ( e1 @ op ) )
         != e1 )
        & ( ( e0 @ ( e0 @ op ) )
         != e0 ) ) ),
    inference(neg_conjecture,[status(cth)],[1]) ).

thf(8,plain,
    ~ ( ( ( ( ( e6 @ ( e6 @ op ) )
           != e6 )
          | ( ( e5 @ ( e5 @ op ) )
           != e5 )
          | ( ( e4 @ ( e4 @ op ) )
           != e4 )
          | ( ( e3 @ ( e3 @ op ) )
           != e3 )
          | ( ( e2 @ ( e2 @ op ) )
           != e2 )
          | ( ( e1 @ ( e1 @ op ) )
           != e1 )
          | ( ( e0 @ ( e0 @ op ) )
           != e0 ) )
        & ( ( ( e6 @ ( e6 @ op ) )
            = e6 )
          | ( ( e5 @ ( e5 @ op ) )
            = e5 )
          | ( ( e4 @ ( e4 @ op ) )
            = e4 )
          | ( ( e3 @ ( e3 @ op ) )
            = e3 )
          | ( ( e2 @ ( e2 @ op ) )
            = e2 )
          | ( ( e1 @ ( e1 @ op ) )
            = e1 )
          | ( ( e0 @ ( e0 @ op ) )
            = e0 ) ) )
      | ( ( ( e6 @ ( e6 @ op ) )
          = e6 )
        & ( ( e5 @ ( e5 @ op ) )
          = e5 )
        & ( ( e4 @ ( e4 @ op ) )
          = e4 )
        & ( ( e3 @ ( e3 @ op ) )
          = e3 )
        & ( ( e2 @ ( e2 @ op ) )
          = e2 )
        & ( ( e1 @ ( e1 @ op ) )
          = e1 )
        & ( ( e0 @ ( e0 @ op ) )
          = e0 ) )
      | ( ( ( e6 @ ( e6 @ op ) )
         != e6 )
        & ( ( e5 @ ( e5 @ op ) )
         != e5 )
        & ( ( e4 @ ( e4 @ op ) )
         != e4 )
        & ( ( e3 @ ( e3 @ op ) )
         != e3 )
        & ( ( e2 @ ( e2 @ op ) )
         != e2 )
        & ( ( e1 @ ( e1 @ op ) )
         != e1 )
        & ( ( e0 @ ( e0 @ op ) )
         != e0 ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).

thf(7,axiom,
    ( ( e5 != e6 )
    & ( e4 != e6 )
    & ( e4 != e5 )
    & ( e3 != e6 )
    & ( e3 != e5 )
    & ( e3 != e4 )
    & ( e2 != e6 )
    & ( e2 != e5 )
    & ( e2 != e4 )
    & ( e2 != e3 )
    & ( e1 != e6 )
    & ( e1 != e5 )
    & ( e1 != e4 )
    & ( e1 != e3 )
    & ( e1 != e2 )
    & ( e0 != e6 )
    & ( e0 != e5 )
    & ( e0 != e4 )
    & ( e0 != e3 )
    & ( e0 != e2 )
    & ( e0 != e1 ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).

thf(1030,plain,
    ( ( e5 != e6 )
    & ( e4 != e6 )
    & ( e4 != e5 )
    & ( e3 != e6 )
    & ( e3 != e5 )
    & ( e3 != e4 )
    & ( e2 != e6 )
    & ( e2 != e5 )
    & ( e2 != e4 )
    & ( e2 != e3 )
    & ( e1 != e6 )
    & ( e1 != e5 )
    & ( e1 != e4 )
    & ( e1 != e3 )
    & ( e1 != e2 )
    & ( e0 != e6 )
    & ( e0 != e5 )
    & ( e0 != e4 )
    & ( e0 != e3 )
    & ( e0 != e2 )
    & ( e0 != e1 ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).

thf(1126,plain,
    $false,
    inference(e,[status(thm)],[440,42,142,340,8,1030]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05  % Problem  : ALG194+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.13  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.26/0.53  % Computer : n007.cluster.edu
% 0.26/0.53  % Model    : x86_64 x86_64
% 0.26/0.53  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.26/0.53  % Memory   : 8046.5625MB
% 0.26/0.53  % OS       : Linux 6.8.0-71-generic
% 0.26/0.53  % CPULimit : 300
% 0.26/0.53  % WCLimit  : 300
% 0.26/0.53  % DateTime : Sat Sep 26 21:22:39 UTC 2026
% 0.26/0.53  % CPUTime  : 
% 0.26/0.54  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.51/1.43  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 2.80/1.93  % [INFO] 	 Parsing done (501ms). 
% 2.80/1.95  % [INFO] 	 Running in sequential loop mode. 
% 4.39/2.58  % [INFO] 	 eprover registered as external prover. 
% 4.39/2.59  % [INFO] 	 Scanning for conjecture ... 
% 5.43/2.88  % [INFO] 	 Found a conjecture (or negated_conjecture) and 5 axioms. Running axiom selection ... 
% 5.88/2.96  % [INFO] 	 Axiom selection finished. Selected 5 axioms (removed 0 axioms). 
% 9.03/4.61  % [INFO] 	 Problem is first-order (TPTP FOF). 
% 9.03/4.66  % [INFO] 	 Type checking passed. 
% 9.03/4.67  % [CONFIG] 	 Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>.  Searching for refutation ... 
% 20.25/8.20  % External prover 'e' found a proof!
% 20.25/8.20  % [INFO] 	 Killing All external provers ... 
% 20.25/8.20  % Time passed: 7446ms (effective reasoning time: 6238ms)
% 20.25/8.20  % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 20.25/8.20  % Axioms used in derivation (5): ax4, ax1, ax2, ax3, ax5
% 20.25/8.20  % No. of inferences in proof: 14
% 20.25/8.20  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 7446 ms resp. 6238 ms w/o parsing
% 20.74/8.30  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 20.74/8.31  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------