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

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : ALG028+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 : n001.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:45:56 AM UTC 2026

% Result   : Theorem 15.42s 6.39s
% Output   : Refutation 16.33s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    3
%            Number of leaves      :   12
% Syntax   : Number of formulae    :   26 (   3 unt;   0 typ;   0 def)
%            Number of atoms       : 1777 (1776 equ;   0 cnn)
%            Maximal formula atoms :  216 (  68 avg)
%            Number of connectives : 9225 ( 428   ~; 430   |;1255   &;7046   @)
%                                         (   0 <=>;  66  =>;   0  <=;   0 <~>)
%            Maximal formula depth :  216 (  51 avg)
%            Number of types       :    1 (   0 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :   11 (   9 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(unit_decl,type,
    unit: $i ).

thf(inv_decl,type,
    inv: $i > $i ).

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

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

thf(9,axiom,
    ( ( ( ( e5 @ inv )
        = e5 )
     => ( ( e5 @ inv )
        = e5 ) )
    & ( ( ( e5 @ inv )
        = e4 )
     => ( ( e4 @ inv )
        = e5 ) )
    & ( ( ( e5 @ inv )
        = e3 )
     => ( ( e3 @ inv )
        = e5 ) )
    & ( ( ( e5 @ inv )
        = e2 )
     => ( ( e2 @ inv )
        = e5 ) )
    & ( ( ( e5 @ inv )
        = e1 )
     => ( ( e1 @ inv )
        = e5 ) )
    & ( ( ( e5 @ inv )
        = e0 )
     => ( ( e0 @ inv )
        = e5 ) )
    & ( ( ( e4 @ inv )
        = e5 )
     => ( ( e5 @ inv )
        = e4 ) )
    & ( ( ( e4 @ inv )
        = e4 )
     => ( ( e4 @ inv )
        = e4 ) )
    & ( ( ( e4 @ inv )
        = e3 )
     => ( ( e3 @ inv )
        = e4 ) )
    & ( ( ( e4 @ inv )
        = e2 )
     => ( ( e2 @ inv )
        = e4 ) )
    & ( ( ( e4 @ inv )
        = e1 )
     => ( ( e1 @ inv )
        = e4 ) )
    & ( ( ( e4 @ inv )
        = e0 )
     => ( ( e0 @ inv )
        = e4 ) )
    & ( ( ( e3 @ inv )
        = e5 )
     => ( ( e5 @ inv )
        = e3 ) )
    & ( ( ( e3 @ inv )
        = e4 )
     => ( ( e4 @ inv )
        = e3 ) )
    & ( ( ( e3 @ inv )
        = e3 )
     => ( ( e3 @ inv )
        = e3 ) )
    & ( ( ( e3 @ inv )
        = e2 )
     => ( ( e2 @ inv )
        = e3 ) )
    & ( ( ( e3 @ inv )
        = e1 )
     => ( ( e1 @ inv )
        = e3 ) )
    & ( ( ( e3 @ inv )
        = e0 )
     => ( ( e0 @ inv )
        = e3 ) )
    & ( ( ( e2 @ inv )
        = e5 )
     => ( ( e5 @ inv )
        = e2 ) )
    & ( ( ( e2 @ inv )
        = e4 )
     => ( ( e4 @ inv )
        = e2 ) )
    & ( ( ( e2 @ inv )
        = e3 )
     => ( ( e3 @ inv )
        = e2 ) )
    & ( ( ( e2 @ inv )
        = e2 )
     => ( ( e2 @ inv )
        = e2 ) )
    & ( ( ( e2 @ inv )
        = e1 )
     => ( ( e1 @ inv )
        = e2 ) )
    & ( ( ( e2 @ inv )
        = e0 )
     => ( ( e0 @ inv )
        = e2 ) )
    & ( ( ( e1 @ inv )
        = e5 )
     => ( ( e5 @ inv )
        = e1 ) )
    & ( ( ( e1 @ inv )
        = e4 )
     => ( ( e4 @ inv )
        = e1 ) )
    & ( ( ( e1 @ inv )
        = e3 )
     => ( ( e3 @ inv )
        = e1 ) )
    & ( ( ( e1 @ inv )
        = e2 )
     => ( ( e2 @ inv )
        = e1 ) )
    & ( ( ( e1 @ inv )
        = e1 )
     => ( ( e1 @ inv )
        = e1 ) )
    & ( ( ( e1 @ inv )
        = e0 )
     => ( ( e0 @ inv )
        = e1 ) )
    & ( ( ( e0 @ inv )
        = e5 )
     => ( ( e5 @ inv )
        = e0 ) )
    & ( ( ( e0 @ inv )
        = e4 )
     => ( ( e4 @ inv )
        = e0 ) )
    & ( ( ( e0 @ inv )
        = e3 )
     => ( ( e3 @ inv )
        = e0 ) )
    & ( ( ( e0 @ inv )
        = e2 )
     => ( ( e2 @ inv )
        = e0 ) )
    & ( ( ( e0 @ inv )
        = e1 )
     => ( ( e1 @ inv )
        = e0 ) )
    & ( ( ( e0 @ inv )
        = e0 )
     => ( ( e0 @ inv )
        = e0 ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7) ).

thf(670,plain,
    ( ( ( ( e5 @ inv )
        = e4 )
     => ( ( e4 @ inv )
        = e5 ) )
    & ( ( ( e5 @ inv )
        = e3 )
     => ( ( e3 @ inv )
        = e5 ) )
    & ( ( ( e5 @ inv )
        = e2 )
     => ( ( e2 @ inv )
        = e5 ) )
    & ( ( ( e5 @ inv )
        = e1 )
     => ( ( e1 @ inv )
        = e5 ) )
    & ( ( ( e5 @ inv )
        = e0 )
     => ( ( e0 @ inv )
        = e5 ) )
    & ( ( ( e4 @ inv )
        = e5 )
     => ( ( e5 @ inv )
        = e4 ) )
    & ( ( ( e4 @ inv )
        = e3 )
     => ( ( e3 @ inv )
        = e4 ) )
    & ( ( ( e4 @ inv )
        = e2 )
     => ( ( e2 @ inv )
        = e4 ) )
    & ( ( ( e4 @ inv )
        = e1 )
     => ( ( e1 @ inv )
        = e4 ) )
    & ( ( ( e4 @ inv )
        = e0 )
     => ( ( e0 @ inv )
        = e4 ) )
    & ( ( ( e3 @ inv )
        = e5 )
     => ( ( e5 @ inv )
        = e3 ) )
    & ( ( ( e3 @ inv )
        = e4 )
     => ( ( e4 @ inv )
        = e3 ) )
    & ( ( ( e3 @ inv )
        = e2 )
     => ( ( e2 @ inv )
        = e3 ) )
    & ( ( ( e3 @ inv )
        = e1 )
     => ( ( e1 @ inv )
        = e3 ) )
    & ( ( ( e3 @ inv )
        = e0 )
     => ( ( e0 @ inv )
        = e3 ) )
    & ( ( ( e2 @ inv )
        = e5 )
     => ( ( e5 @ inv )
        = e2 ) )
    & ( ( ( e2 @ inv )
        = e4 )
     => ( ( e4 @ inv )
        = e2 ) )
    & ( ( ( e2 @ inv )
        = e3 )
     => ( ( e3 @ inv )
        = e2 ) )
    & ( ( ( e2 @ inv )
        = e1 )
     => ( ( e1 @ inv )
        = e2 ) )
    & ( ( ( e2 @ inv )
        = e0 )
     => ( ( e0 @ inv )
        = e2 ) )
    & ( ( ( e1 @ inv )
        = e5 )
     => ( ( e5 @ inv )
        = e1 ) )
    & ( ( ( e1 @ inv )
        = e4 )
     => ( ( e4 @ inv )
        = e1 ) )
    & ( ( ( e1 @ inv )
        = e3 )
     => ( ( e3 @ inv )
        = e1 ) )
    & ( ( ( e1 @ inv )
        = e2 )
     => ( ( e2 @ inv )
        = e1 ) )
    & ( ( ( e1 @ inv )
        = e0 )
     => ( ( e0 @ inv )
        = e1 ) )
    & ( ( ( e0 @ inv )
        = e5 )
     => ( ( e5 @ inv )
        = e0 ) )
    & ( ( ( e0 @ inv )
        = e4 )
     => ( ( e4 @ inv )
        = e0 ) )
    & ( ( ( e0 @ inv )
        = e3 )
     => ( ( e3 @ inv )
        = e0 ) )
    & ( ( ( e0 @ inv )
        = e2 )
     => ( ( e2 @ inv )
        = e0 ) )
    & ( ( ( e0 @ inv )
        = e1 )
     => ( ( e1 @ inv )
        = e0 ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).

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

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

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

thf(7,axiom,
    ( ( unit @ inv )
    = unit ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).

thf(654,plain,
    ( ( unit @ inv )
    = unit ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).

thf(10,axiom,
    ( ( ( e4 @ inv )
     != ( e5 @ inv ) )
    & ( ( e3 @ inv )
     != ( e5 @ inv ) )
    & ( ( e3 @ inv )
     != ( e4 @ inv ) )
    & ( ( e2 @ inv )
     != ( e5 @ inv ) )
    & ( ( e2 @ inv )
     != ( e4 @ inv ) )
    & ( ( e2 @ inv )
     != ( e3 @ inv ) )
    & ( ( e1 @ inv )
     != ( e5 @ inv ) )
    & ( ( e1 @ inv )
     != ( e4 @ inv ) )
    & ( ( e1 @ inv )
     != ( e3 @ inv ) )
    & ( ( e1 @ inv )
     != ( e2 @ inv ) )
    & ( ( e0 @ inv )
     != ( e5 @ inv ) )
    & ( ( e0 @ inv )
     != ( e4 @ inv ) )
    & ( ( e0 @ inv )
     != ( e3 @ inv ) )
    & ( ( e0 @ inv )
     != ( e2 @ inv ) )
    & ( ( e0 @ inv )
     != ( e1 @ inv ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8) ).

thf(732,plain,
    ( ( ( e4 @ inv )
     != ( e5 @ inv ) )
    & ( ( e3 @ inv )
     != ( e5 @ inv ) )
    & ( ( e3 @ inv )
     != ( e4 @ inv ) )
    & ( ( e2 @ inv )
     != ( e5 @ inv ) )
    & ( ( e2 @ inv )
     != ( e4 @ inv ) )
    & ( ( e2 @ inv )
     != ( e3 @ inv ) )
    & ( ( e1 @ inv )
     != ( e5 @ inv ) )
    & ( ( e1 @ inv )
     != ( e4 @ inv ) )
    & ( ( e1 @ inv )
     != ( e3 @ inv ) )
    & ( ( e1 @ inv )
     != ( e2 @ inv ) )
    & ( ( e0 @ inv )
     != ( e5 @ inv ) )
    & ( ( e0 @ inv )
     != ( e4 @ inv ) )
    & ( ( e0 @ inv )
     != ( e3 @ inv ) )
    & ( ( e0 @ inv )
     != ( e2 @ inv ) )
    & ( ( e0 @ inv )
     != ( e1 @ inv ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).

thf(3,axiom,
    ( ( ( ( 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 ) )
        = e5 )
      | ( ( e4 @ ( e5 @ op ) )
        = e4 )
      | ( ( e4 @ ( e5 @ op ) )
        = e3 )
      | ( ( e4 @ ( e5 @ op ) )
        = e2 )
      | ( ( e4 @ ( e5 @ op ) )
        = e1 )
      | ( ( e4 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e2 @ ( e5 @ op ) )
        = e4 )
      | ( ( e2 @ ( e5 @ op ) )
        = e3 )
      | ( ( e2 @ ( e5 @ op ) )
        = e2 )
      | ( ( e2 @ ( e5 @ op ) )
        = e1 )
      | ( ( e2 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e0 @ ( e5 @ op ) )
        = e4 )
      | ( ( e0 @ ( e5 @ op ) )
        = e3 )
      | ( ( e0 @ ( e5 @ op ) )
        = e2 )
      | ( ( e0 @ ( e5 @ op ) )
        = e1 )
      | ( ( e0 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e4 @ ( e4 @ op ) )
        = e4 )
      | ( ( e4 @ ( e4 @ op ) )
        = e3 )
      | ( ( e4 @ ( e4 @ op ) )
        = e2 )
      | ( ( e4 @ ( e4 @ op ) )
        = e1 )
      | ( ( e4 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e2 @ ( e4 @ op ) )
        = e4 )
      | ( ( e2 @ ( e4 @ op ) )
        = e3 )
      | ( ( e2 @ ( e4 @ op ) )
        = e2 )
      | ( ( e2 @ ( e4 @ op ) )
        = e1 )
      | ( ( e2 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e0 @ ( e4 @ op ) )
        = e4 )
      | ( ( e0 @ ( e4 @ op ) )
        = e3 )
      | ( ( e0 @ ( e4 @ op ) )
        = e2 )
      | ( ( e0 @ ( e4 @ op ) )
        = e1 )
      | ( ( e0 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e4 @ ( e3 @ op ) )
        = e4 )
      | ( ( e4 @ ( e3 @ op ) )
        = e3 )
      | ( ( e4 @ ( e3 @ op ) )
        = e2 )
      | ( ( e4 @ ( e3 @ op ) )
        = e1 )
      | ( ( e4 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e2 @ ( e3 @ op ) )
        = e4 )
      | ( ( e2 @ ( e3 @ op ) )
        = e3 )
      | ( ( e2 @ ( e3 @ op ) )
        = e2 )
      | ( ( e2 @ ( e3 @ op ) )
        = e1 )
      | ( ( e2 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e0 @ ( e3 @ op ) )
        = e4 )
      | ( ( e0 @ ( e3 @ op ) )
        = e3 )
      | ( ( e0 @ ( e3 @ op ) )
        = e2 )
      | ( ( e0 @ ( e3 @ op ) )
        = e1 )
      | ( ( e0 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e4 @ ( e2 @ op ) )
        = e4 )
      | ( ( e4 @ ( e2 @ op ) )
        = e3 )
      | ( ( e4 @ ( e2 @ op ) )
        = e2 )
      | ( ( e4 @ ( e2 @ op ) )
        = e1 )
      | ( ( e4 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e2 @ ( e2 @ op ) )
        = e4 )
      | ( ( e2 @ ( e2 @ op ) )
        = e3 )
      | ( ( e2 @ ( e2 @ op ) )
        = e2 )
      | ( ( e2 @ ( e2 @ op ) )
        = e1 )
      | ( ( e2 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e0 @ ( e2 @ op ) )
        = e4 )
      | ( ( e0 @ ( e2 @ op ) )
        = e3 )
      | ( ( e0 @ ( e2 @ op ) )
        = e2 )
      | ( ( e0 @ ( e2 @ op ) )
        = e1 )
      | ( ( e0 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e4 @ ( e1 @ op ) )
        = e4 )
      | ( ( e4 @ ( e1 @ op ) )
        = e3 )
      | ( ( e4 @ ( e1 @ op ) )
        = e2 )
      | ( ( e4 @ ( e1 @ op ) )
        = e1 )
      | ( ( e4 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e2 @ ( e1 @ op ) )
        = e4 )
      | ( ( e2 @ ( e1 @ op ) )
        = e3 )
      | ( ( e2 @ ( e1 @ op ) )
        = e2 )
      | ( ( e2 @ ( e1 @ op ) )
        = e1 )
      | ( ( e2 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e0 @ ( e1 @ op ) )
        = e4 )
      | ( ( e0 @ ( e1 @ op ) )
        = e3 )
      | ( ( e0 @ ( e1 @ op ) )
        = e2 )
      | ( ( e0 @ ( e1 @ op ) )
        = e1 )
      | ( ( e0 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e4 @ ( e0 @ op ) )
        = e4 )
      | ( ( e4 @ ( e0 @ op ) )
        = e3 )
      | ( ( e4 @ ( e0 @ op ) )
        = e2 )
      | ( ( e4 @ ( e0 @ op ) )
        = e1 )
      | ( ( e4 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e2 @ ( e0 @ op ) )
        = e4 )
      | ( ( e2 @ ( e0 @ op ) )
        = e3 )
      | ( ( e2 @ ( e0 @ op ) )
        = e2 )
      | ( ( e2 @ ( e0 @ op ) )
        = e1 )
      | ( ( e2 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = 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(80,plain,
    ( ( ( ( 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 ) )
        = e5 )
      | ( ( e4 @ ( e5 @ op ) )
        = e4 )
      | ( ( e4 @ ( e5 @ op ) )
        = e3 )
      | ( ( e4 @ ( e5 @ op ) )
        = e2 )
      | ( ( e4 @ ( e5 @ op ) )
        = e1 )
      | ( ( e4 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e2 @ ( e5 @ op ) )
        = e4 )
      | ( ( e2 @ ( e5 @ op ) )
        = e3 )
      | ( ( e2 @ ( e5 @ op ) )
        = e2 )
      | ( ( e2 @ ( e5 @ op ) )
        = e1 )
      | ( ( e2 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e0 @ ( e5 @ op ) )
        = e4 )
      | ( ( e0 @ ( e5 @ op ) )
        = e3 )
      | ( ( e0 @ ( e5 @ op ) )
        = e2 )
      | ( ( e0 @ ( e5 @ op ) )
        = e1 )
      | ( ( e0 @ ( e5 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e4 @ ( e4 @ op ) )
        = e4 )
      | ( ( e4 @ ( e4 @ op ) )
        = e3 )
      | ( ( e4 @ ( e4 @ op ) )
        = e2 )
      | ( ( e4 @ ( e4 @ op ) )
        = e1 )
      | ( ( e4 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e2 @ ( e4 @ op ) )
        = e4 )
      | ( ( e2 @ ( e4 @ op ) )
        = e3 )
      | ( ( e2 @ ( e4 @ op ) )
        = e2 )
      | ( ( e2 @ ( e4 @ op ) )
        = e1 )
      | ( ( e2 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e0 @ ( e4 @ op ) )
        = e4 )
      | ( ( e0 @ ( e4 @ op ) )
        = e3 )
      | ( ( e0 @ ( e4 @ op ) )
        = e2 )
      | ( ( e0 @ ( e4 @ op ) )
        = e1 )
      | ( ( e0 @ ( e4 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e4 @ ( e3 @ op ) )
        = e4 )
      | ( ( e4 @ ( e3 @ op ) )
        = e3 )
      | ( ( e4 @ ( e3 @ op ) )
        = e2 )
      | ( ( e4 @ ( e3 @ op ) )
        = e1 )
      | ( ( e4 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e2 @ ( e3 @ op ) )
        = e4 )
      | ( ( e2 @ ( e3 @ op ) )
        = e3 )
      | ( ( e2 @ ( e3 @ op ) )
        = e2 )
      | ( ( e2 @ ( e3 @ op ) )
        = e1 )
      | ( ( e2 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e0 @ ( e3 @ op ) )
        = e4 )
      | ( ( e0 @ ( e3 @ op ) )
        = e3 )
      | ( ( e0 @ ( e3 @ op ) )
        = e2 )
      | ( ( e0 @ ( e3 @ op ) )
        = e1 )
      | ( ( e0 @ ( e3 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e4 @ ( e2 @ op ) )
        = e4 )
      | ( ( e4 @ ( e2 @ op ) )
        = e3 )
      | ( ( e4 @ ( e2 @ op ) )
        = e2 )
      | ( ( e4 @ ( e2 @ op ) )
        = e1 )
      | ( ( e4 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e2 @ ( e2 @ op ) )
        = e4 )
      | ( ( e2 @ ( e2 @ op ) )
        = e3 )
      | ( ( e2 @ ( e2 @ op ) )
        = e2 )
      | ( ( e2 @ ( e2 @ op ) )
        = e1 )
      | ( ( e2 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e0 @ ( e2 @ op ) )
        = e4 )
      | ( ( e0 @ ( e2 @ op ) )
        = e3 )
      | ( ( e0 @ ( e2 @ op ) )
        = e2 )
      | ( ( e0 @ ( e2 @ op ) )
        = e1 )
      | ( ( e0 @ ( e2 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e4 @ ( e1 @ op ) )
        = e4 )
      | ( ( e4 @ ( e1 @ op ) )
        = e3 )
      | ( ( e4 @ ( e1 @ op ) )
        = e2 )
      | ( ( e4 @ ( e1 @ op ) )
        = e1 )
      | ( ( e4 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e2 @ ( e1 @ op ) )
        = e4 )
      | ( ( e2 @ ( e1 @ op ) )
        = e3 )
      | ( ( e2 @ ( e1 @ op ) )
        = e2 )
      | ( ( e2 @ ( e1 @ op ) )
        = e1 )
      | ( ( e2 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e0 @ ( e1 @ op ) )
        = e4 )
      | ( ( e0 @ ( e1 @ op ) )
        = e3 )
      | ( ( e0 @ ( e1 @ op ) )
        = e2 )
      | ( ( e0 @ ( e1 @ op ) )
        = e1 )
      | ( ( e0 @ ( e1 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e4 @ ( e0 @ op ) )
        = e4 )
      | ( ( e4 @ ( e0 @ op ) )
        = e3 )
      | ( ( e4 @ ( e0 @ op ) )
        = e2 )
      | ( ( e4 @ ( e0 @ op ) )
        = e1 )
      | ( ( e4 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = e5 )
      | ( ( e2 @ ( e0 @ op ) )
        = e4 )
      | ( ( e2 @ ( e0 @ op ) )
        = e3 )
      | ( ( e2 @ ( e0 @ op ) )
        = e2 )
      | ( ( e2 @ ( e0 @ op ) )
        = e1 )
      | ( ( e2 @ ( e0 @ op ) )
        = e0 ) )
    & ( ( ( 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 ) )
        = 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(12,axiom,
    ( ( e4 != e5 )
    & ( e3 != e5 )
    & ( e3 != e4 )
    & ( e2 != e5 )
    & ( e2 != e4 )
    & ( e2 != e3 )
    & ( e1 != e5 )
    & ( e1 != e4 )
    & ( e1 != e3 )
    & ( e1 != e2 )
    & ( e0 != e5 )
    & ( e0 != e4 )
    & ( e0 != e3 )
    & ( e0 != e2 )
    & ( e0 != e1 ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).

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

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

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

thf(11,axiom,
    ( ( ( e4 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e5 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e3 @ ( 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 ) )
     != ( 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 ) ) )
    & ( ( e4 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e3 @ ( 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 ) )
     != ( 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 ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e3 @ ( 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 ) )
     != ( 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 ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e3 @ ( 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 ) )
     != ( 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 ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e3 @ ( 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 ) )
     != ( 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 ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e4 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e4 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e3 @ ( 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 ) )
     != ( 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 ) ) )
    & ( ( e5 @ ( e4 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e3 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e3 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e3 @ 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 @ ( 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 @ ( e4 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e3 @ 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 @ ( 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 @ ( e4 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e3 @ 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 @ ( 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 @ ( e4 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e3 @ 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 @ ( 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 @ ( e4 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e3 @ 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 @ ( 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 @ ( e4 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e0 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e3 @ 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 @ ( 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',ax9) ).

thf(764,plain,
    ( ( ( e4 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e5 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e5 @ op ) )
     != ( e3 @ ( 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 ) )
     != ( 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 ) ) )
    & ( ( e4 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e4 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e4 @ op ) )
     != ( e3 @ ( 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 ) )
     != ( 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 ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e5 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e4 @ ( e3 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e3 @ ( 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 ) )
     != ( 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 ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e5 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e4 @ ( e2 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e3 @ ( 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 ) )
     != ( 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 ) ) )
    & ( ( e4 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e3 @ ( e1 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e5 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e4 @ ( e1 @ op ) ) )
    & ( ( e2 @ ( e1 @ op ) )
     != ( e3 @ ( 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 ) )
     != ( 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 ) ) )
    & ( ( e4 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e3 @ ( e0 @ op ) )
     != ( e4 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e5 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e4 @ ( e0 @ op ) ) )
    & ( ( e2 @ ( e0 @ op ) )
     != ( e3 @ ( 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 ) )
     != ( 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 ) ) )
    & ( ( e5 @ ( e4 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e3 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e3 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e5 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e4 @ op ) ) )
    & ( ( e5 @ ( e2 @ op ) )
     != ( e5 @ ( e3 @ 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 @ ( 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 @ ( e4 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e3 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e5 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e4 @ op ) ) )
    & ( ( e4 @ ( e2 @ op ) )
     != ( e4 @ ( e3 @ 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 @ ( 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 @ ( e4 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e3 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e5 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e4 @ op ) ) )
    & ( ( e3 @ ( e2 @ op ) )
     != ( e3 @ ( e3 @ 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 @ ( 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 @ ( e4 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e3 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e5 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e4 @ op ) ) )
    & ( ( e2 @ ( e2 @ op ) )
     != ( e2 @ ( e3 @ 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 @ ( 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 @ ( e4 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e3 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e5 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e4 @ op ) ) )
    & ( ( e1 @ ( e2 @ op ) )
     != ( e1 @ ( e3 @ 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 @ ( 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 @ ( e4 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e3 @ op ) )
     != ( e0 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e5 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e4 @ op ) ) )
    & ( ( e0 @ ( e2 @ op ) )
     != ( e0 @ ( e3 @ 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 @ ( 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)],[11]) ).

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

thf(616,plain,
    ( ( ( ( e5 @ inv )
        = e5 )
      | ( ( e5 @ inv )
        = e4 )
      | ( ( e5 @ inv )
        = e3 )
      | ( ( e5 @ inv )
        = e2 )
      | ( ( e5 @ inv )
        = e1 )
      | ( ( e5 @ inv )
        = e0 ) )
    & ( ( ( e4 @ inv )
        = e5 )
      | ( ( e4 @ inv )
        = e4 )
      | ( ( e4 @ inv )
        = e3 )
      | ( ( e4 @ inv )
        = e2 )
      | ( ( e4 @ inv )
        = e1 )
      | ( ( e4 @ inv )
        = e0 ) )
    & ( ( ( e3 @ inv )
        = e5 )
      | ( ( e3 @ inv )
        = e4 )
      | ( ( e3 @ inv )
        = e3 )
      | ( ( e3 @ inv )
        = e2 )
      | ( ( e3 @ inv )
        = e1 )
      | ( ( e3 @ inv )
        = e0 ) )
    & ( ( ( e2 @ inv )
        = e5 )
      | ( ( e2 @ inv )
        = e4 )
      | ( ( e2 @ inv )
        = e3 )
      | ( ( e2 @ inv )
        = e2 )
      | ( ( e2 @ inv )
        = e1 )
      | ( ( e2 @ inv )
        = e0 ) )
    & ( ( ( e1 @ inv )
        = e5 )
      | ( ( e1 @ inv )
        = e4 )
      | ( ( e1 @ inv )
        = e3 )
      | ( ( e1 @ inv )
        = e2 )
      | ( ( e1 @ inv )
        = e1 )
      | ( ( e1 @ inv )
        = e0 ) )
    & ( ( ( e0 @ inv )
        = e5 )
      | ( ( e0 @ inv )
        = e4 )
      | ( ( e0 @ inv )
        = e3 )
      | ( ( e0 @ inv )
        = e2 )
      | ( ( e0 @ inv )
        = e1 )
      | ( ( e0 @ inv )
        = e0 ) )
    & ( ( e5 @ ( e5 @ inv @ op ) )
      = unit )
    & ( ( e5 @ inv @ ( e5 @ op ) )
      = unit )
    & ( ( e4 @ ( e4 @ inv @ op ) )
      = unit )
    & ( ( e4 @ inv @ ( e4 @ op ) )
      = unit )
    & ( ( e3 @ ( e3 @ inv @ op ) )
      = unit )
    & ( ( e3 @ inv @ ( e3 @ op ) )
      = unit )
    & ( ( e2 @ ( e2 @ inv @ op ) )
      = unit )
    & ( ( e2 @ inv @ ( e2 @ op ) )
      = unit )
    & ( ( e1 @ ( e1 @ inv @ op ) )
      = unit )
    & ( ( e1 @ inv @ ( e1 @ op ) )
      = unit )
    & ( ( e0 @ ( e0 @ inv @ op ) )
      = unit )
    & ( ( e0 @ inv @ ( e0 @ op ) )
      = unit ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).

thf(8,axiom,
    ( ( ( e5 @ inv @ inv )
      = e5 )
    & ( ( e4 @ inv @ inv )
      = e4 )
    & ( ( e3 @ inv @ inv )
      = e3 )
    & ( ( e2 @ inv @ inv )
      = e2 )
    & ( ( e1 @ inv @ inv )
      = e1 )
    & ( ( e0 @ inv @ inv )
      = e0 ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).

thf(656,plain,
    ( ( ( e5 @ inv @ inv )
      = e5 )
    & ( ( e4 @ inv @ inv )
      = e4 )
    & ( ( e3 @ inv @ inv )
      = e3 )
    & ( ( e2 @ inv @ inv )
      = e2 )
    & ( ( e1 @ inv @ inv )
      = e1 )
    & ( ( e0 @ inv @ inv )
      = e0 ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).

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

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

thf(1176,plain,
    $false,
    inference(e,[status(thm)],[1158,670,14,654,732,80,1126,588,764,616,656,154]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ALG028+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.08  % 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.15/0.40  % Computer : n001.cluster.edu
% 0.15/0.40  % Model    : x86_64 x86_64
% 0.15/0.40  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.40  % Memory   : 8046.5625MB
% 0.15/0.40  % OS       : Linux 6.8.0-71-generic
% 0.15/0.40  % CPULimit : 300
% 0.15/0.41  % WCLimit  : 300
% 0.15/0.41  % DateTime : Sat Sep 26 21:05:29 UTC 2026
% 0.15/0.41  % CPUTime  : 
% 0.15/0.41  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
% 0.71/0.77  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 1.17/0.98  % [INFO] 	 Parsing done (209ms). 
% 1.17/0.99  % [INFO] 	 Running in sequential loop mode. 
% 2.30/1.23  % [INFO] 	 eprover registered as external prover. 
% 2.30/1.24  % [INFO] 	 Scanning for conjecture ... 
% 3.42/1.54  % [INFO] 	 Found a conjecture (or negated_conjecture) and 11 axioms. Running axiom selection ... 
% 3.85/1.60  % [INFO] 	 Axiom selection finished. Selected 11 axioms (removed 0 axioms). 
% 5.16/2.28  % [INFO] 	 Problem is first-order (TPTP FOF). 
% 5.39/2.30  % [INFO] 	 Type checking passed. 
% 5.39/2.31  % [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 ... 
% 15.42/6.39  % External prover 'e' found a proof!
% 15.42/6.39  % [INFO] 	 Killing All external provers ... 
% 15.42/6.39  % Time passed: 5848ms (effective reasoning time: 5394ms)
% 15.42/6.39  % 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)>
% 15.42/6.39  % Axioms used in derivation (11): ax4, ax9, ax6, ax8, ax10, ax11, ax2, ax1, ax7, ax3, ax5
% 15.42/6.39  % No. of inferences in proof: 26
% 15.42/6.39  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 5848 ms resp. 5394 ms w/o parsing
% 16.33/6.59  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 16.33/6.59  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------