Leo-III---1.8.0.UNS-Ref.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : LCL103-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39

% Computer : n006.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 07:50:49 AM UTC 2026

% Result   : Unsatisfiable 91.86s 31.83s
% Output   : Refutation 96.01s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   51
%            Number of leaves      :    4
% Syntax   : Number of formulae    :  507 ( 193 unt;   0 typ;   0 def)
%            Number of atoms       : 1551 ( 644 equ;   0 cnn)
%            Maximal formula atoms :    9 (   3 avg)
%            Number of connectives : 11868 ( 789   ~; 616   |;   0   &;10463   @)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   21 (  11 avg)
%            Number of types       :    2 (   0 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :    9 (   6 usr;   6 con; 0-2 aty)
%            Number of variables   : 2192 (   0   ^;2192   !;   0   ?;2192   :)

% Comments : 
%------------------------------------------------------------------------------
thf(is_a_theorem_decl,type,
    is_a_theorem: $i > $o ).

thf(equivalent_decl,type,
    equivalent: $i > $i > $i ).

thf(a_decl,type,
    a: $i ).

thf(b_decl,type,
    b: $i ).

thf(c_decl,type,
    c: $i ).

thf(e_decl,type,
    e: $i ).

thf(3,axiom,
    ! [D: $i,C: $i,B: $i,A: $i] : ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p_1) ).

thf(9,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).

thf(2,axiom,
    ! [B: $i,A: $i] :
      ( ( B @ is_a_theorem )
      | ~ ( A @ is_a_theorem )
      | ~ ( B @ ( A @ equivalent ) @ is_a_theorem ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).

thf(7,plain,
    ! [B: $i,A: $i] :
      ( ( B @ is_a_theorem )
      | ~ ( A @ is_a_theorem )
      | ~ ( B @ ( A @ equivalent ) @ is_a_theorem ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).

thf(8,plain,
    ! [B: $i,A: $i] :
      ( ( B @ is_a_theorem )
      | ~ ( A @ is_a_theorem )
      | ~ ( B @ ( A @ equivalent ) @ is_a_theorem ) ),
    inference(cnf,[status(esa)],[7]) ).

thf(28,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem )
      | ~ ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[9,8]) ).

thf(29,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem )
      | ~ ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[28]) ).

thf(30,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( D @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[29:[bind(A,$thf( Q )),bind(B,$thf( N )),bind(C,$thf( P )),bind(D,$thf( R )),bind(E,$thf( P @ ( N @ ( Q @ equivalent ) @ equivalent ) )),bind(F,$thf( P @ ( R @ ( Q @ equivalent ) @ equivalent ) @ ( N @ ( R @ equivalent ) @ equivalent ) ))]]) ).

thf(40,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( D @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[30]) ).

thf(156,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[9,40]) ).

thf(157,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[156]) ).

thf(158,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( E @ equivalent ) @ equivalent ) @ ( A @ ( B @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[157:[bind(A,$thf( Q )),bind(B,$thf( N )),bind(C,$thf( P )),bind(D,$thf( R )),bind(E,$thf( P )),bind(F,$thf( P @ ( R @ ( Q @ equivalent ) @ equivalent ) @ ( N @ ( R @ equivalent ) @ equivalent ) )),bind(G,$thf( N @ ( Q @ equivalent ) )),bind(H,$thf( H ))]]) ).

thf(200,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( E @ equivalent ) @ equivalent ) @ ( A @ ( B @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[158]) ).

thf(4,axiom,
    ! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q_3) ).

thf(10,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).

thf(22,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ ( D @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[10,8]) ).

thf(23,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[22]) ).

thf(24,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ is_a_theorem )
      | ~ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[23:[bind(A,$thf( M )),bind(B,$thf( L )),bind(C,$thf( K )),bind(D,$thf( K @ ( M @ ( L @ equivalent ) @ equivalent ) @ ( L @ ( M @ equivalent ) @ equivalent ) )),bind(E,$thf( K ))]]) ).

thf(38,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ is_a_theorem )
      | ~ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[24]) ).

thf(399,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( E @ equivalent ) @ equivalent ) @ ( A @ ( B @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[200,38]) ).

thf(400,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( E @ equivalent ) @ equivalent ) @ ( A @ ( B @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem ) ),
    inference(simp,[status(thm)],[399]) ).

thf(401,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[400:[bind(A,$thf( A )),bind(B,$thf( T )),bind(C,$thf( T @ ( S @ equivalent ) )),bind(D,$thf( S )),bind(E,$thf( R )),bind(F,$thf( T @ ( S @ equivalent ) @ ( R @ ( S @ equivalent ) @ equivalent ) @ ( T @ ( R @ equivalent ) @ equivalent ) )),bind(G,$thf( T @ ( S @ equivalent ) )),bind(H,$thf( A ))]]) ).

thf(419,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[401]) ).

thf(433,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[419,40]) ).

thf(434,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[433]) ).

thf(435,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[434:[bind(A,$thf( K )),bind(B,$thf( L )),bind(C,$thf( M )),bind(D,$thf( M )),bind(E,$thf( M @ ( L @ equivalent ) @ ( K @ ( L @ equivalent ) @ equivalent ) )),bind(F,$thf( K )),bind(G,$thf( G ))]]) ).

thf(462,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[435]) ).

thf(25,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true
      | ~ ( E @ ( D @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[10,8]) ).

thf(26,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ ( E @ ( D @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[25]) ).

thf(27,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ is_a_theorem )
      | ~ ( A @ ( B @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[26:[bind(A,$thf( O )),bind(B,$thf( N )),bind(C,$thf( G )),bind(D,$thf( G @ ( G @ ( O @ ( N @ equivalent ) @ equivalent ) @ ( N @ ( O @ equivalent ) @ equivalent ) @ equivalent ) )),bind(E,$thf( E ))]]) ).

thf(39,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ is_a_theorem )
      | ~ ( A @ ( B @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[27]) ).

thf(70,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[9,39]) ).

thf(71,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[70]) ).

thf(72,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[71:[bind(A,$thf( ZB @ ( ZA @ equivalent ) )),bind(B,$thf( X @ ( ZA @ ( ZB @ equivalent ) @ equivalent ) )),bind(C,$thf( X )),bind(D,$thf( Z )),bind(E,$thf( X @ ( Z @ ( ZB @ ( ZA @ equivalent ) @ equivalent ) @ equivalent ) @ ( X @ ( ZA @ ( ZB @ equivalent ) @ equivalent ) @ ( Z @ equivalent ) @ equivalent ) )),bind(F,$thf( X )),bind(G,$thf( ZB )),bind(H,$thf( ZA ))]]) ).

thf(74,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[72]) ).

thf(34,plain,
    ! [B: $i,A: $i] :
      ( ~ $true
      | ( ( B @ ( A @ equivalent ) @ is_a_theorem )
       != ( A @ is_a_theorem ) )
      | ( B @ is_a_theorem )
      | ~ ( A @ is_a_theorem ) ),
    inference(eqfactor_ordered,[status(thm)],[8]) ).

thf(35,plain,
    ! [B: $i,A: $i] :
      ( ( ( B @ ( A @ equivalent ) @ is_a_theorem )
       != ( A @ is_a_theorem ) )
      | ~ ( A @ is_a_theorem )
      | ( B @ is_a_theorem ) ),
    inference(simp,[status(thm)],[34]) ).

thf(83,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ equivalent ) @ is_a_theorem ) )
      | ~ ( E @ is_a_theorem )
      | ~ ( E @ is_a_theorem )
      | ( F @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[74,35]) ).

thf(84,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ equivalent ) @ is_a_theorem ) )
      | ~ ( E @ is_a_theorem )
      | ( F @ is_a_theorem ) ),
    inference(simp,[status(thm)],[83]) ).

thf(85,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ~ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ is_a_theorem )
      | ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[84:[bind(A,$thf( N )),bind(B,$thf( P )),bind(C,$thf( Q )),bind(D,$thf( R )),bind(E,$thf( N @ ( Q @ ( R @ equivalent ) @ equivalent ) @ ( P @ equivalent ) )),bind(F,$thf( N @ ( P @ ( R @ ( Q @ equivalent ) @ equivalent ) @ equivalent ) ))]]) ).

thf(97,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ~ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ is_a_theorem )
      | ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[85]) ).

thf(1960,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[462,97]) ).

thf(1961,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1960]) ).

thf(1962,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1961:[bind(A,$thf( I )),bind(B,$thf( N )),bind(C,$thf( O )),bind(D,$thf( P )),bind(E,$thf( P @ ( O @ equivalent ) @ ( N @ ( O @ equivalent ) @ equivalent ) )),bind(F,$thf( P @ ( I @ equivalent ) )),bind(G,$thf( I )),bind(H,$thf( N ))]]) ).

thf(2043,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1962]) ).

thf(31,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ is_a_theorem ) )
      | ( F @ is_a_theorem )
      | ~ $true
      | ~ ( F @ ( E @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[9,8]) ).

thf(32,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ is_a_theorem ) )
      | ( F @ is_a_theorem )
      | ~ ( F @ ( E @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[31]) ).

thf(33,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ is_a_theorem )
      | ~ ( A @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[32:[bind(A,$thf( S )),bind(B,$thf( P )),bind(C,$thf( R )),bind(D,$thf( T )),bind(E,$thf( R @ ( T @ ( S @ equivalent ) @ equivalent ) @ ( P @ ( T @ equivalent ) @ equivalent ) @ ( R @ ( P @ ( S @ equivalent ) @ equivalent ) @ equivalent ) )),bind(F,$thf( F ))]]) ).

thf(37,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ is_a_theorem )
      | ~ ( A @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[33]) ).

thf(2817,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( F @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2043,37]) ).

thf(2818,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( F @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2817]) ).

thf(2819,plain,
    ! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2818:[bind(A,$thf( K @ ( Y @ equivalent ) )),bind(B,$thf( W )),bind(C,$thf( T )),bind(D,$thf( W @ ( Y @ ( Y @ equivalent ) @ equivalent ) )),bind(E,$thf( W @ ( Y @ ( Y @ equivalent ) @ equivalent ) @ ( T @ equivalent ) @ ( W @ ( T @ equivalent ) @ equivalent ) )),bind(F,$thf( K )),bind(G,$thf( W )),bind(H,$thf( Y )),bind(I,$thf( Y ))]]) ).

thf(2857,plain,
    ! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2819]) ).

thf(441,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( E @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[419,39]) ).

thf(442,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( E @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[441]) ).

thf(443,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( D @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[442:[bind(A,$thf( ZC @ ( ZA @ ( Z @ equivalent ) @ equivalent ) @ ( Z @ ( ZA @ equivalent ) @ equivalent ) )),bind(B,$thf( ZB )),bind(C,$thf( ZC )),bind(D,$thf( ZC @ ( ZB @ equivalent ) @ ( ZC @ ( ZA @ ( Z @ equivalent ) @ equivalent ) @ ( Z @ ( ZA @ equivalent ) @ equivalent ) @ ( ZB @ equivalent ) @ equivalent ) )),bind(E,$thf( ZC )),bind(F,$thf( Z )),bind(G,$thf( ZA ))]]) ).

thf(467,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( D @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[443]) ).

thf(553,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( D @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( F @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[467,37]) ).

thf(554,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( D @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( F @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[553]) ).

thf(555,plain,
    ! [B: $i,A: $i] : ( A @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[554:[bind(A,$thf( S )),bind(B,$thf( B )),bind(C,$thf( O @ ( S @ ( S @ equivalent ) @ equivalent ) )),bind(D,$thf( O )),bind(E,$thf( O @ ( O @ ( S @ ( S @ equivalent ) @ equivalent ) @ equivalent ) )),bind(F,$thf( S )),bind(G,$thf( O )),bind(H,$thf( S )),bind(I,$thf( B ))]]) ).

thf(587,plain,
    ! [B: $i,A: $i] : ( A @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[555]) ).

thf(594,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( C @ ( E @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[587,40]) ).

thf(595,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( C @ ( E @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[594]) ).

thf(596,plain,
    ! [C: $i,B: $i,A: $i] : ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[595:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( A )),bind(D,$thf( A )),bind(E,$thf( H @ ( H @ equivalent ) )),bind(F,$thf( F ))]]) ).

thf(624,plain,
    ! [C: $i,B: $i,A: $i] : ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[596]) ).

thf(643,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( E @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[624,39]) ).

thf(644,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( E @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[643]) ).

thf(645,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[644:[bind(A,$thf( Q )),bind(B,$thf( Q @ ( ZC @ ( ZB @ equivalent ) @ equivalent ) @ ( ZB @ ( ZC @ equivalent ) @ equivalent ) )),bind(C,$thf( U )),bind(D,$thf( Q @ ( Q @ ( ZC @ ( ZB @ equivalent ) @ equivalent ) @ ( ZB @ ( ZC @ equivalent ) @ equivalent ) @ ( U @ ( U @ equivalent ) @ equivalent ) @ equivalent ) )),bind(E,$thf( Q )),bind(F,$thf( ZB )),bind(G,$thf( ZC ))]]) ).

thf(665,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[645]) ).

thf(682,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[665,40]) ).

thf(683,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[682]) ).

thf(684,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[683:[bind(A,$thf( P )),bind(B,$thf( J )),bind(C,$thf( Q )),bind(D,$thf( R )),bind(E,$thf( P @ ( R @ ( Q @ equivalent ) @ equivalent ) @ ( Q @ ( R @ equivalent ) @ equivalent ) )),bind(F,$thf( P )),bind(G,$thf( J @ ( J @ equivalent ) )),bind(H,$thf( H ))]]) ).

thf(714,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[684]) ).

thf(1394,plain,
    ! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( J @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( J @ equivalent ) @ equivalent ) @ ( H @ ( G @ ( I @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[714,37]) ).

thf(1395,plain,
    ! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( J @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( J @ equivalent ) @ equivalent ) @ ( H @ ( G @ ( I @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1394]) ).

thf(1396,plain,
    ! [C: $i,B: $i,A: $i] : ( A @ ( A @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1395:[bind(A,$thf( P @ ( X @ ( X @ equivalent ) @ equivalent ) )),bind(B,$thf( T )),bind(C,$thf( P )),bind(D,$thf( X )),bind(E,$thf( E )),bind(F,$thf( P @ ( P @ ( X @ ( X @ equivalent ) @ equivalent ) @ ( T @ ( T @ equivalent ) @ equivalent ) @ equivalent ) )),bind(G,$thf( X )),bind(H,$thf( P )),bind(I,$thf( X )),bind(J,$thf( E ))]]) ).

thf(1426,plain,
    ! [C: $i,B: $i,A: $i] : ( A @ ( A @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1396]) ).

thf(1433,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[1426,40]) ).

thf(1434,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1433]) ).

thf(1435,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( C @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1434:[bind(A,$thf( K )),bind(B,$thf( I )),bind(C,$thf( M )),bind(D,$thf( K @ ( M @ ( M @ equivalent ) @ equivalent ) )),bind(E,$thf( K )),bind(F,$thf( I @ ( I @ equivalent ) )),bind(G,$thf( G ))]]) ).

thf(1468,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( C @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1435]) ).

thf(2023,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[1468,97]) ).

thf(2024,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2023]) ).

thf(2025,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( D @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2024:[bind(A,$thf( I )),bind(B,$thf( P )),bind(C,$thf( L )),bind(D,$thf( N )),bind(E,$thf( L )),bind(F,$thf( L @ ( N @ ( N @ equivalent ) @ equivalent ) @ ( I @ equivalent ) )),bind(G,$thf( I )),bind(H,$thf( P @ ( P @ equivalent ) ))]]) ).

thf(2072,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( D @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2025]) ).

thf(1,negated_conjecture,
    ~ ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_lg_2) ).

thf(5,plain,
    ~ ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).

thf(6,plain,
    ~ ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(polarity_switch,[status(thm)],[5]) ).

thf(75,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[74,6]) ).

thf(76,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[75]) ).

thf(95,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[76]) ).

thf(130,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) )
       != e )
      | ( ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) )
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[95]) ).

thf(202,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) )
       != e )
      | ( ( A @ ( C @ ( D @ equivalent ) @ equivalent ) )
       != e )
      | ( B
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[130]) ).

thf(203,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( A @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ equivalent ) )
       != e )
      | ( ( A @ ( B @ ( C @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[202]) ).

thf(204,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( e != e )
      | ( ( A @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ equivalent ) )
       != ( A @ ( B @ ( C @ equivalent ) @ equivalent ) ) )
      | ( ( A @ ( B @ ( C @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(eqfactor_ordered,[status(thm)],[203]) ).

thf(206,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A != A )
      | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) )
       != ( B @ ( C @ equivalent ) ) )
      | ( ( A @ ( B @ ( C @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[204]) ).

thf(207,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) )
       != ( B @ ( C @ equivalent ) ) )
      | ( ( A @ ( B @ ( C @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[206]) ).

thf(243,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
       != B )
      | ( ( C @ ( B @ equivalent ) )
       != C )
      | ( ( A @ ( B @ ( C @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[207]) ).

thf(244,plain,
    ! [B: $i,A: $i] :
      ( ( ( B @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
       != B )
      | ( ( A @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[243]) ).

thf(245,plain,
    ! [B: $i,A: $i] :
      ( ( e != B )
      | ( ( A @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) )
       != ( B @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) )
      | ( ( B @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
       != B ) ),
    inference(eqfactor_ordered,[status(thm)],[244]) ).

thf(247,plain,
    ! [A: $i] :
      ( ( A != e )
      | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) )
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) )
      | ( ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[245]) ).

thf(248,plain,
    ( ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) )
     != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) )
    | ( ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[247]) ).

thf(381,plain,
    ( ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( c @ ( b @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e )
    | ( ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[248]) ).

thf(383,plain,
    ( ( e != e )
    | ( ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( c @ ( b @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(eqfactor_ordered,[status(thm)],[381]) ).

thf(387,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[383]) ).

thf(628,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a )
    | ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[387]) ).

thf(1909,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ~ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[97,6]) ).

thf(1910,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1909]) ).

thf(1911,plain,
    ~ ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1910:[bind(A,$thf( e )),bind(B,$thf( e )),bind(C,$thf( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )),bind(D,$thf( c @ ( b @ equivalent ) ))]]) ).

thf(2094,plain,
    ! [B: $i,A: $i] :
      ( ( ( A @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[587,1911]) ).

thf(2095,plain,
    ! [B: $i,A: $i] :
      ( ( A @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2094]) ).

thf(2195,plain,
    ! [B: $i,A: $i] :
      ( ( A @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) ) ),
    inference(simp,[status(thm)],[2095]) ).

thf(2362,plain,
    ! [B: $i,A: $i] :
      ( ( A
       != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) ) )
      | ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[2195]) ).

thf(2363,plain,
    ! [A: $i] :
      ( ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) )
     != e ),
    inference(simp,[status(thm)],[2362]) ).

thf(2014,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[624,97]) ).

thf(2015,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2014]) ).

thf(2016,plain,
    ! [C: $i,B: $i,A: $i] : ( B @ ( B @ ( A @ equivalent ) @ ( C @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2015:[bind(A,$thf( I )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( I )),bind(E,$thf( I @ ( H @ equivalent ) )),bind(F,$thf( H )),bind(G,$thf( K @ ( K @ equivalent ) ))]]) ).

thf(2066,plain,
    ! [C: $i,B: $i,A: $i] : ( B @ ( B @ ( A @ equivalent ) @ ( C @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2016]) ).

thf(2315,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( B @ ( A @ equivalent ) @ ( C @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2066,37]) ).

thf(2316,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( B @ ( A @ equivalent ) @ ( C @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2315]) ).

thf(2317,plain,
    ! [B: $i,A: $i] : ( B @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2316:[bind(A,$thf( J @ ( V @ equivalent ) )),bind(B,$thf( X @ ( X @ equivalent ) @ ( V @ ( V @ equivalent ) @ equivalent ) )),bind(C,$thf( X )),bind(D,$thf( X @ ( X @ equivalent ) @ ( V @ ( V @ equivalent ) @ equivalent ) )),bind(E,$thf( J )),bind(F,$thf( X @ ( X @ equivalent ) )),bind(G,$thf( V )),bind(H,$thf( V ))]]) ).

thf(2358,plain,
    ! [B: $i,A: $i] : ( B @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2317]) ).

thf(2387,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( C @ ( E @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2358,40]) ).

thf(2388,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( C @ ( E @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2387]) ).

thf(2389,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( C @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2388:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( A )),bind(D,$thf( H @ ( H @ equivalent ) )),bind(E,$thf( A )),bind(F,$thf( F ))]]) ).

thf(2409,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( C @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2389]) ).

thf(2479,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[2409,97]) ).

thf(2480,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2479]) ).

thf(2481,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( C @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2480:[bind(A,$thf( I )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( K @ ( K @ equivalent ) )),bind(E,$thf( I @ ( H @ equivalent ) )),bind(F,$thf( H )),bind(G,$thf( I ))]]) ).

thf(2512,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( C @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2481]) ).

thf(520,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[462,39]) ).

thf(521,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[520]) ).

thf(522,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( E @ ( D @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( E @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[521:[bind(A,$thf( ZH @ ( ZB @ ( ZA @ equivalent ) @ equivalent ) @ ( ZA @ ( ZB @ equivalent ) @ equivalent ) )),bind(B,$thf( ZF )),bind(C,$thf( ZG )),bind(D,$thf( ZH )),bind(E,$thf( ZH @ ( ZG @ equivalent ) @ ( ZF @ ( ZG @ equivalent ) @ equivalent ) @ ( ZH @ ( ZB @ ( ZA @ equivalent ) @ equivalent ) @ ( ZA @ ( ZB @ equivalent ) @ equivalent ) @ ( ZF @ equivalent ) @ equivalent ) )),bind(F,$thf( ZH )),bind(G,$thf( ZA )),bind(H,$thf( ZB ))]]) ).

thf(545,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( E @ ( D @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( E @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[522]) ).

thf(983,plain,
    ! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( E @ ( D @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( E @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( J @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( J @ equivalent ) @ equivalent ) @ ( H @ ( G @ ( I @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[545,37]) ).

thf(984,plain,
    ! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( E @ ( D @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( E @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( J @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( J @ equivalent ) @ equivalent ) @ ( H @ ( G @ ( I @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem ) ),
    inference(simp,[status(thm)],[983]) ).

thf(985,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( B @ equivalent ) @ ( C @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[984:[bind(A,$thf( V )),bind(B,$thf( B )),bind(C,$thf( X @ ( V @ ( V @ equivalent ) @ equivalent ) )),bind(D,$thf( W )),bind(E,$thf( X )),bind(F,$thf( X @ ( W @ equivalent ) @ ( X @ ( V @ ( V @ equivalent ) @ equivalent ) @ ( W @ equivalent ) @ equivalent ) )),bind(G,$thf( V )),bind(H,$thf( X )),bind(I,$thf( V )),bind(J,$thf( B ))]]) ).

thf(1019,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( B @ equivalent ) @ ( C @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[985]) ).

thf(1033,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[1019,6]) ).

thf(1034,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1033]) ).

thf(1056,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[1034]) ).

thf(1068,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) )
       != e )
      | ( ( C @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( B @ equivalent ) )
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[1056]) ).

thf(386,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( c @ ( b @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[383]) ).

thf(1198,plain,
    ( ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(eqfactor_ordered,[status(thm)],[386]) ).

thf(1207,plain,
    ( ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[1198]) ).

thf(2579,plain,
    ( ( ( b @ ( a @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( c @ ( b @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(eqfactor_ordered,[status(thm)],[1207]) ).

thf(2590,plain,
    ( ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b )
    | ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[2579]) ).

thf(1948,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[419,97]) ).

thf(1949,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1948]) ).

thf(1950,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( B @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1949:[bind(A,$thf( H )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( K @ ( J @ equivalent ) )),bind(E,$thf( K @ ( H @ equivalent ) )),bind(F,$thf( H )),bind(G,$thf( J ))]]) ).

thf(2039,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( B @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1950]) ).

thf(2227,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2039,40]) ).

thf(2228,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2227]) ).

thf(2229,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( D @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2228:[bind(A,$thf( J )),bind(B,$thf( L )),bind(C,$thf( M )),bind(D,$thf( M @ ( J @ equivalent ) )),bind(E,$thf( M @ ( L @ equivalent ) )),bind(F,$thf( L @ ( J @ equivalent ) )),bind(G,$thf( G ))]]) ).

thf(2248,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( D @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2229]) ).

thf(251,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( F @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[74,37]) ).

thf(252,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( F @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[251]) ).

thf(253,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[252:[bind(A,$thf( ZC @ ( ZE @ ( ZD @ equivalent ) @ equivalent ) )),bind(B,$thf( ZC @ ( ZA @ ( ZD @ equivalent ) @ equivalent ) )),bind(C,$thf( ZA )),bind(D,$thf( ZE )),bind(E,$thf( ZC @ ( ZE @ ( ZD @ equivalent ) @ equivalent ) @ ( ZC @ ( ZA @ ( ZD @ equivalent ) @ equivalent ) @ ( ZE @ ( ZA @ equivalent ) @ equivalent ) @ equivalent ) )),bind(F,$thf( ZA )),bind(G,$thf( ZC )),bind(H,$thf( ZD )),bind(I,$thf( ZE ))]]) ).

thf(270,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[253]) ).

thf(309,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[270,39]) ).

thf(310,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[309]) ).

thf(311,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( D @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[310:[bind(A,$thf( ZH @ ( ZG @ equivalent ) )),bind(B,$thf( V )),bind(C,$thf( ZE )),bind(D,$thf( V @ ( ZH @ ( ZG @ equivalent ) @ ( ZE @ equivalent ) @ equivalent ) @ ( ZG @ ( ZH @ equivalent ) @ equivalent ) )),bind(E,$thf( V @ ( V @ ( ZH @ ( ZG @ equivalent ) @ ( ZE @ equivalent ) @ equivalent ) @ ( ZG @ ( ZH @ equivalent ) @ equivalent ) @ ( ZE @ equivalent ) @ equivalent ) )),bind(F,$thf( V @ ( ZH @ ( ZG @ equivalent ) @ ( ZE @ equivalent ) @ equivalent ) )),bind(G,$thf( ZH )),bind(H,$thf( ZG ))]]) ).

thf(339,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( D @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[311]) ).

thf(349,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( D @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[339,40]) ).

thf(350,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( D @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[349]) ).

thf(351,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( E @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[350:[bind(A,$thf( N )),bind(B,$thf( O )),bind(C,$thf( Q )),bind(D,$thf( R )),bind(E,$thf( N @ ( R @ ( Q @ equivalent ) @ ( O @ equivalent ) @ equivalent ) @ ( Q @ ( R @ equivalent ) @ equivalent ) )),bind(F,$thf( N )),bind(G,$thf( O )),bind(H,$thf( H ))]]) ).

thf(379,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( E @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[351]) ).

thf(597,plain,
    ! [B: $i,A: $i] :
      ( ( ( A @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[587,6]) ).

thf(598,plain,
    ! [B: $i,A: $i] :
      ( ( A @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[597]) ).

thf(619,plain,
    ! [B: $i,A: $i] :
      ( ( A @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[598]) ).

thf(671,plain,
    ! [B: $i,A: $i] :
      ( ( A != e )
      | ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[619]) ).

thf(672,plain,
    ! [A: $i] :
      ( ( e @ ( A @ ( A @ equivalent ) @ equivalent ) )
     != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[671]) ).

thf(673,plain,
    ! [A: $i] :
      ( ( e != e )
      | ( ( A @ ( A @ equivalent ) )
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[672]) ).

thf(674,plain,
    ! [A: $i] :
      ( ( A @ ( A @ equivalent ) )
     != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[673]) ).

thf(675,plain,
    ! [A: $i] :
      ( ( A
       != ( c @ ( b @ equivalent ) ) )
      | ( A
       != ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[674]) ).

thf(676,plain,
    ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
   != ( c @ ( b @ equivalent ) ) ),
    inference(simp,[status(thm)],[675]) ).

thf(677,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != c )
    | ( ( b @ ( a @ equivalent ) )
     != b ) ),
    inference(simp,[status(thm)],[676]) ).

thf(385,plain,
    ( ( ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[383]) ).

thf(436,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[419,6]) ).

thf(437,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[436]) ).

thf(459,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[437]) ).

thf(548,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) )
       != e )
      | ( ( C @ ( A @ equivalent ) )
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[459]) ).

thf(549,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) )
       != e )
      | ( C != e )
      | ( A
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[548]) ).

thf(550,plain,
    ! [A: $i] :
      ( ( e @ ( A @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) )
     != e ),
    inference(simp,[status(thm)],[549]) ).

thf(2491,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2409,40]) ).

thf(2492,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2491]) ).

thf(2493,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2492:[bind(A,$thf( J )),bind(B,$thf( K )),bind(C,$thf( M )),bind(D,$thf( J )),bind(E,$thf( M @ ( M @ equivalent ) @ ( K @ ( J @ equivalent ) @ equivalent ) )),bind(F,$thf( K )),bind(G,$thf( G ))]]) ).

thf(2516,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2493]) ).

thf(632,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[624,37]) ).

thf(633,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[632]) ).

thf(634,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[633:[bind(A,$thf( ZJ @ ( ZL @ ( ZK @ equivalent ) @ equivalent ) @ ( ZH @ ( ZL @ equivalent ) @ equivalent ) )),bind(B,$thf( ZJ @ ( ZH @ ( ZK @ equivalent ) @ equivalent ) )),bind(C,$thf( Z )),bind(D,$thf( ZJ @ ( ZL @ ( ZK @ equivalent ) @ equivalent ) @ ( ZH @ ( ZL @ equivalent ) @ equivalent ) @ ( ZJ @ ( ZH @ ( ZK @ equivalent ) @ equivalent ) @ ( Z @ ( Z @ equivalent ) @ equivalent ) @ equivalent ) )),bind(E,$thf( ZH )),bind(F,$thf( ZJ )),bind(G,$thf( ZK )),bind(H,$thf( ZL ))]]) ).

thf(667,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[634]) ).

thf(1231,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[667,38]) ).

thf(1232,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1231]) ).

thf(1233,plain,
    ! [C: $i,B: $i,A: $i] : ( A @ ( A @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1232:[bind(A,$thf( ZD )),bind(B,$thf( ZD @ ( ZD @ equivalent ) )),bind(C,$thf( V )),bind(D,$thf( ZA )),bind(E,$thf( V @ ( ZD @ ( ZD @ equivalent ) @ ( ZA @ equivalent ) @ equivalent ) )),bind(F,$thf( V @ ( V @ ( ZD @ ( ZD @ equivalent ) @ ( ZA @ equivalent ) @ equivalent ) @ ( ZA @ equivalent ) @ equivalent ) )),bind(G,$thf( V @ ( ZD @ ( ZD @ equivalent ) @ ( ZA @ equivalent ) @ equivalent ) )),bind(H,$thf( ZD @ ( ZD @ equivalent ) ))]]) ).

thf(1254,plain,
    ! [C: $i,B: $i,A: $i] : ( A @ ( A @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1233]) ).

thf(2371,plain,
    ! [B: $i,A: $i] :
      ( ( ( B @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2358,6]) ).

thf(2372,plain,
    ! [B: $i,A: $i] :
      ( ( B @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2371]) ).

thf(2402,plain,
    ! [B: $i,A: $i] :
      ( ( B @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[2372]) ).

thf(2755,plain,
    ! [B: $i,A: $i] :
      ( ( ( B @ ( B @ equivalent ) )
       != e )
      | ( ( A @ ( A @ equivalent ) )
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[2402]) ).

thf(77,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[74,39]) ).

thf(78,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[77]) ).

thf(79,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[78:[bind(A,$thf( V )),bind(B,$thf( V @ ( ZL @ ( ZK @ equivalent ) @ equivalent ) @ ( ZH @ ( ZG @ equivalent ) @ equivalent ) @ ( ZG @ ( ZH @ equivalent ) @ equivalent ) )),bind(C,$thf( ZL )),bind(D,$thf( ZK )),bind(E,$thf( V @ ( V @ ( ZL @ ( ZK @ equivalent ) @ equivalent ) @ ( ZH @ ( ZG @ equivalent ) @ equivalent ) @ ( ZG @ ( ZH @ equivalent ) @ equivalent ) @ ( ZK @ ( ZL @ equivalent ) @ equivalent ) @ equivalent ) )),bind(F,$thf( V @ ( ZL @ ( ZK @ equivalent ) @ equivalent ) )),bind(G,$thf( ZG )),bind(H,$thf( ZH ))]]) ).

thf(100,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[79]) ).

thf(119,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[100,6]) ).

thf(120,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[119]) ).

thf(125,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[120]) ).

thf(2204,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2039,37]) ).

thf(2205,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2204]) ).

thf(2206,plain,
    ! [B: $i,A: $i] : ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2205:[bind(A,$thf( J @ ( T @ equivalent ) )),bind(B,$thf( R )),bind(C,$thf( R @ ( T @ ( T @ equivalent ) @ equivalent ) )),bind(D,$thf( R @ ( T @ ( T @ equivalent ) @ equivalent ) @ ( R @ equivalent ) )),bind(E,$thf( J )),bind(F,$thf( R )),bind(G,$thf( T )),bind(H,$thf( T ))]]) ).

thf(2251,plain,
    ! [B: $i,A: $i] : ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2206]) ).

thf(2253,plain,
    ! [B: $i,A: $i] :
      ( ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem )
       != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2251,1911]) ).

thf(2254,plain,
    ! [B: $i,A: $i] :
      ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem )
     != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2253]) ).

thf(2293,plain,
    ! [B: $i,A: $i] :
      ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) )
     != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) ) ),
    inference(simp,[status(thm)],[2254]) ).

thf(2570,plain,
    ! [B: $i,A: $i] :
      ( ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) ) )
      | ( A != e ) ),
    inference(simp,[status(thm)],[2293]) ).

thf(2571,plain,
    ! [A: $i] :
      ( ( e @ ( A @ ( A @ equivalent ) @ equivalent ) )
     != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[2570]) ).

thf(430,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[419,37]) ).

thf(431,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[430]) ).

thf(432,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[431:[bind(A,$thf( ZJ @ ( ZH @ ( ZK @ equivalent ) @ equivalent ) )),bind(B,$thf( ZC )),bind(C,$thf( ZJ @ ( ZL @ ( ZK @ equivalent ) @ equivalent ) @ ( ZH @ ( ZL @ equivalent ) @ equivalent ) )),bind(D,$thf( ZJ @ ( ZL @ ( ZK @ equivalent ) @ equivalent ) @ ( ZH @ ( ZL @ equivalent ) @ equivalent ) @ ( ZC @ equivalent ) @ ( ZJ @ ( ZH @ ( ZK @ equivalent ) @ equivalent ) @ ( ZC @ equivalent ) @ equivalent ) )),bind(E,$thf( ZH )),bind(F,$thf( ZJ )),bind(G,$thf( ZK )),bind(H,$thf( ZL ))]]) ).

thf(460,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[432]) ).

thf(2376,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( C @ ( E @ ( F @ equivalent ) @ equivalent ) @ ( D @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( C @ ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[2358,97]) ).

thf(2377,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( C @ ( E @ ( F @ equivalent ) @ equivalent ) @ ( D @ equivalent ) @ is_a_theorem ) )
      | ( C @ ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2376]) ).

thf(2378,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2377:[bind(A,$thf( H )),bind(B,$thf( L @ ( K @ equivalent ) )),bind(C,$thf( L @ ( K @ equivalent ) )),bind(D,$thf( H @ ( H @ equivalent ) )),bind(E,$thf( L )),bind(F,$thf( K ))]]) ).

thf(2406,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2378]) ).

thf(2438,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2406,40]) ).

thf(2439,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2438]) ).

thf(2440,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2439:[bind(A,$thf( K )),bind(B,$thf( L )),bind(C,$thf( M )),bind(D,$thf( K @ ( K @ equivalent ) )),bind(E,$thf( M @ ( L @ equivalent ) )),bind(F,$thf( L @ ( M @ equivalent ) )),bind(G,$thf( G ))]]) ).

thf(2456,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2440]) ).

thf(45,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ is_a_theorem ) )
      | ( ( E @ ( D @ equivalent ) @ is_a_theorem )
       != ( D @ is_a_theorem ) )
      | ~ $true
      | ( E @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[10,35]) ).

thf(46,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ is_a_theorem ) )
      | ( ( E @ ( D @ equivalent ) @ is_a_theorem )
       != ( D @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[45]) ).

thf(47,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( B @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( A @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[46:[bind(A,$thf( O )),bind(B,$thf( N )),bind(C,$thf( G )),bind(D,$thf( G @ ( G @ ( O @ ( N @ equivalent ) @ equivalent ) @ ( N @ ( O @ equivalent ) @ equivalent ) @ equivalent ) )),bind(E,$thf( E ))]]) ).

thf(61,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( B @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( A @ is_a_theorem ) ),
    inference(simp,[status(thm)],[47]) ).

thf(153,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[74,40]) ).

thf(154,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[153]) ).

thf(155,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( B @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[154:[bind(A,$thf( N )),bind(B,$thf( P )),bind(C,$thf( Q )),bind(D,$thf( R )),bind(E,$thf( N @ ( Q @ ( R @ equivalent ) @ equivalent ) )),bind(F,$thf( N @ ( P @ ( R @ ( Q @ equivalent ) @ equivalent ) @ equivalent ) )),bind(G,$thf( P )),bind(H,$thf( H ))]]) ).

thf(198,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( B @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[155]) ).

thf(222,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[198,38]) ).

thf(223,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem ) ),
    inference(simp,[status(thm)],[222]) ).

thf(224,plain,
    ! [C: $i,B: $i,A: $i] : ( A @ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[223:[bind(A,$thf( A )),bind(B,$thf( R )),bind(C,$thf( R @ ( Z @ ( Y @ equivalent ) @ equivalent ) )),bind(D,$thf( Z )),bind(E,$thf( Y )),bind(F,$thf( R @ ( R @ ( Z @ ( Y @ equivalent ) @ equivalent ) @ ( Y @ ( Z @ equivalent ) @ equivalent ) @ equivalent ) )),bind(G,$thf( R @ ( Z @ ( Y @ equivalent ) @ equivalent ) )),bind(H,$thf( A ))]]) ).

thf(235,plain,
    ! [C: $i,B: $i,A: $i] : ( A @ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[224]) ).

thf(278,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[235,6]) ).

thf(279,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[278]) ).

thf(299,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[279]) ).

thf(427,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A != e )
      | ( ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[299]) ).

thf(428,plain,
    ! [B: $i,A: $i] :
      ( ( e @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) )
     != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[427]) ).

thf(80,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ is_a_theorem ) )
      | ( ( F @ ( E @ equivalent ) @ is_a_theorem )
       != ( E @ is_a_theorem ) )
      | ~ $true
      | ( F @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[74,35]) ).

thf(81,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ is_a_theorem ) )
      | ( ( F @ ( E @ equivalent ) @ is_a_theorem )
       != ( E @ is_a_theorem ) )
      | ( F @ is_a_theorem ) ),
    inference(simp,[status(thm)],[80]) ).

thf(82,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( B @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( A @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[81:[bind(A,$thf( P )),bind(B,$thf( R )),bind(C,$thf( S )),bind(D,$thf( T )),bind(E,$thf( P @ ( R @ ( T @ ( S @ equivalent ) @ equivalent ) @ equivalent ) @ ( P @ ( S @ ( T @ equivalent ) @ equivalent ) @ ( R @ equivalent ) @ equivalent ) )),bind(F,$thf( F ))]]) ).

thf(96,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( B @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( A @ is_a_theorem ) ),
    inference(simp,[status(thm)],[82]) ).

thf(1604,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ~ ( A @ ( B @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ( A @ is_a_theorem ) ),
    inference(rewrite,[status(thm)],[96,74]) ).

thf(638,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[624,6]) ).

thf(639,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[638]) ).

thf(661,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[639]) ).

thf(759,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) )
       != e )
      | ( ( A @ ( B @ equivalent ) )
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[661]) ).

thf(760,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) )
       != e )
      | ( A != e )
      | ( B
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[759]) ).

thf(761,plain,
    ! [A: $i] :
      ( ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) )
     != e ),
    inference(simp,[status(thm)],[760]) ).

thf(1262,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[1254,40]) ).

thf(1263,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1262]) ).

thf(1264,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1263:[bind(A,$thf( I )),bind(B,$thf( J )),bind(C,$thf( M )),bind(D,$thf( I @ ( M @ ( M @ equivalent ) @ ( J @ equivalent ) @ equivalent ) )),bind(E,$thf( I )),bind(F,$thf( J )),bind(G,$thf( G ))]]) ).

thf(1294,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1264]) ).

thf(1304,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( F @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[1294,37]) ).

thf(1305,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( F @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1304]) ).

thf(1306,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ ( A @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1305:[bind(A,$thf( ZE @ ( ZC @ ( ZC @ equivalent ) @ ( ZF @ equivalent ) @ equivalent ) )),bind(B,$thf( ZE @ ( ZG @ ( ZF @ equivalent ) @ equivalent ) )),bind(C,$thf( ZG )),bind(D,$thf( ZC )),bind(E,$thf( ZE @ ( ZG @ ( ZF @ equivalent ) @ equivalent ) @ ( ZE @ ( ZC @ ( ZC @ equivalent ) @ ( ZF @ equivalent ) @ equivalent ) @ ( ZG @ equivalent ) @ equivalent ) )),bind(F,$thf( ZC @ ( ZC @ equivalent ) )),bind(G,$thf( ZE )),bind(H,$thf( ZF )),bind(I,$thf( ZG ))]]) ).

thf(1338,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ ( A @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1306]) ).

thf(14,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[9,6]) ).

thf(15,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[14]) ).

thf(16,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[15]) ).

thf(41,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) )
       != e )
      | ( ( C @ ( B @ ( A @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[16]) ).

thf(101,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) )
       != e )
      | ( C != e )
      | ( ( B @ ( A @ equivalent ) )
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[41]) ).

thf(102,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( e @ ( C @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) )
       != e )
      | ( ( B @ ( A @ equivalent ) )
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[101]) ).

thf(1208,plain,
    ( ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[1198]) ).

thf(1555,plain,
    ( ( e != e )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( c @ ( a @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a ) ),
    inference(eqfactor_ordered,[status(thm)],[1208]) ).

thf(1556,plain,
    ( ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( c @ ( a @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a ) ),
    inference(simp,[status(thm)],[1555]) ).

thf(4141,plain,
    ( ( ( c @ ( b @ equivalent ) )
     != ( c @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a ) ),
    inference(eqfactor_ordered,[status(thm)],[1556]) ).

thf(4148,plain,
    ( ( c != c )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != b )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a ) ),
    inference(simp,[status(thm)],[4141]) ).

thf(4159,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != b )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a ) ),
    inference(simp,[status(thm)],[4148]) ).

thf(4164,plain,
    ( ( a != a )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != b )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b ) ),
    inference(eqfactor_ordered,[status(thm)],[4159]) ).

thf(4166,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != b )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( ( c @ ( a @ equivalent ) )
     != b )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b ) ),
    inference(simp,[status(thm)],[4164]) ).

thf(4167,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != b )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b ) ),
    inference(simp,[status(thm)],[4166]) ).

thf(4169,plain,
    ( ( b != b )
    | ( ( c @ ( b @ equivalent ) )
     != ( c @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != b )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e ) ),
    inference(eqfactor_ordered,[status(thm)],[4167]) ).

thf(4171,plain,
    ( ( c != c )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != b )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[4169]) ).

thf(4172,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != b )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[4171]) ).

thf(2589,plain,
    ( ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( c @ ( b @ equivalent ) ) )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[2579]) ).

thf(2591,plain,
    ( ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[2579]) ).

thf(2595,plain,
    ( ( e != e )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( c @ ( a @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e ) ),
    inference(eqfactor_ordered,[status(thm)],[2591]) ).

thf(2596,plain,
    ( ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( c @ ( a @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[2595]) ).

thf(629,plain,
    ( ( e != e )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( c @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a )
    | ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b ) ),
    inference(eqfactor_ordered,[status(thm)],[628]) ).

thf(630,plain,
    ( ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( c @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a )
    | ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b ) ),
    inference(simp,[status(thm)],[629]) ).

thf(429,plain,
    ! [B: $i,A: $i] :
      ( ( ( e @ ( B @ ( A @ equivalent ) @ equivalent ) )
       != e )
      | ( ( A @ ( B @ equivalent ) )
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[428]) ).

thf(1269,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[1254,6]) ).

thf(1270,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ ( A @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1269]) ).

thf(1291,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ ( A @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[1270]) ).

thf(1823,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A != e )
      | ( ( A @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( B @ equivalent ) )
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[1291]) ).

thf(1824,plain,
    ! [B: $i,A: $i] :
      ( ( e @ ( B @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ ( A @ equivalent ) )
     != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[1823]) ).

thf(11,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[10,6]) ).

thf(12,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[11]) ).

thf(13,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[12]) ).

thf(17,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( C != e )
      | ( ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[13]) ).

thf(18,plain,
    ! [B: $i,A: $i] :
      ( ( e @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) )
     != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[17]) ).

thf(19,plain,
    ! [B: $i,A: $i] :
      ( ( ( e @ ( A @ ( B @ equivalent ) @ equivalent ) )
       != e )
      | ( ( B @ ( A @ equivalent ) )
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[18]) ).

thf(20,plain,
    ! [B: $i,A: $i] :
      ( ( ( e @ ( A @ ( B @ equivalent ) @ equivalent ) )
       != e )
      | ( B
       != ( c @ ( b @ equivalent ) ) )
      | ( A
       != ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[19]) ).

thf(21,plain,
    ( ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) )
   != e ),
    inference(simp,[status(thm)],[20]) ).

thf(3064,plain,
    ! [B: $i,A: $i] :
      ( ( ( B @ ( B @ equivalent ) )
       != e )
      | ( A != e )
      | ( A
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[2755]) ).

thf(3065,plain,
    ! [A: $i] :
      ( ( ( A @ ( A @ equivalent ) )
       != e )
      | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[3064]) ).

thf(2017,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[1019,97]) ).

thf(2018,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2017]) ).

thf(2019,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2018:[bind(A,$thf( M )),bind(B,$thf( O @ ( N @ equivalent ) )),bind(C,$thf( K )),bind(D,$thf( K )),bind(E,$thf( K @ ( M @ ( M @ equivalent ) @ equivalent ) @ ( O @ ( N @ equivalent ) @ equivalent ) )),bind(F,$thf( O )),bind(G,$thf( N ))]]) ).

thf(2068,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2019]) ).

thf(1210,plain,
    ( ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[1198]) ).

thf(121,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[100,38]) ).

thf(122,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem ) ),
    inference(simp,[status(thm)],[121]) ).

thf(124,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) )
       != ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) ) )
      | ( F @ is_a_theorem ) ),
    inference(simp,[status(thm)],[122]) ).

thf(635,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[624,40]) ).

thf(636,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[635]) ).

thf(637,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[636:[bind(A,$thf( I )),bind(B,$thf( K )),bind(C,$thf( M )),bind(D,$thf( I )),bind(E,$thf( I @ ( K @ ( M @ ( M @ equivalent ) @ equivalent ) @ equivalent ) )),bind(F,$thf( K )),bind(G,$thf( G ))]]) ).

thf(669,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[637]) ).

thf(723,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[669,40]) ).

thf(724,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[723]) ).

thf(725,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( D @ ( E @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[724:[bind(A,$thf( L )),bind(B,$thf( N )),bind(C,$thf( P )),bind(D,$thf( R )),bind(E,$thf( N )),bind(F,$thf( N @ ( P @ ( R @ ( R @ equivalent ) @ equivalent ) @ equivalent ) @ ( L @ ( P @ equivalent ) @ equivalent ) )),bind(G,$thf( L )),bind(H,$thf( H ))]]) ).

thf(753,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( D @ ( E @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[725]) ).

thf(2364,plain,
    ! [B: $i,A: $i] :
      ( ( ( B @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2358,1911]) ).

thf(2365,plain,
    ! [B: $i,A: $i] :
      ( ( B @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
     != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2364]) ).

thf(2401,plain,
    ! [B: $i,A: $i] :
      ( ( B @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) )
     != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) ) ),
    inference(simp,[status(thm)],[2365]) ).

thf(2649,plain,
    ! [B: $i,A: $i] :
      ( ( ( B @ ( B @ equivalent ) )
       != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) ) )
      | ( ( A @ ( A @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[2401]) ).

thf(1069,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) )
       != e )
      | ( ( C @ ( A @ ( A @ equivalent ) @ equivalent ) )
       != e )
      | ( B
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[1068]) ).

thf(1070,plain,
    ! [B: $i,A: $i] :
      ( ( ( B @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
       != e )
      | ( ( B @ ( A @ ( A @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[1069]) ).

thf(1191,plain,
    ! [B: $i,A: $i] :
      ( ( e != e )
      | ( ( B @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
       != ( B @ ( A @ ( A @ equivalent ) @ equivalent ) ) )
      | ( ( B @ ( A @ ( A @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(eqfactor_ordered,[status(thm)],[1070]) ).

thf(1192,plain,
    ! [B: $i,A: $i] :
      ( ( ( B @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
       != ( B @ ( A @ ( A @ equivalent ) @ equivalent ) ) )
      | ( ( B @ ( A @ ( A @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[1191]) ).

thf(1028,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[1019,40]) ).

thf(1029,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1028]) ).

thf(1030,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1029:[bind(A,$thf( K )),bind(B,$thf( L )),bind(C,$thf( M )),bind(D,$thf( M @ ( K @ ( K @ equivalent ) @ equivalent ) )),bind(E,$thf( M @ ( L @ equivalent ) )),bind(F,$thf( L )),bind(G,$thf( G ))]]) ).

thf(1060,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1030]) ).

thf(107,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ is_a_theorem ) )
      | ( ( G @ ( F @ equivalent ) @ is_a_theorem )
       != ( F @ is_a_theorem ) )
      | ~ $true
      | ( G @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[100,35]) ).

thf(108,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ is_a_theorem ) )
      | ( ( G @ ( F @ equivalent ) @ is_a_theorem )
       != ( F @ is_a_theorem ) )
      | ( G @ is_a_theorem ) ),
    inference(simp,[status(thm)],[107]) ).

thf(109,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( B @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( B @ ( B @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( A @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[108:[bind(A,$thf( I )),bind(B,$thf( T )),bind(C,$thf( U )),bind(D,$thf( X )),bind(E,$thf( Y )),bind(F,$thf( I @ ( I @ ( Y @ ( X @ equivalent ) @ equivalent ) @ ( U @ ( T @ equivalent ) @ equivalent ) @ ( T @ ( U @ equivalent ) @ equivalent ) @ ( X @ ( Y @ equivalent ) @ equivalent ) @ equivalent ) )),bind(G,$thf( G ))]]) ).

thf(129,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( B @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( B @ ( B @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( A @ is_a_theorem ) ),
    inference(simp,[status(thm)],[109]) ).

thf(68,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( E @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[10,39]) ).

thf(69,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( E @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[68]) ).

thf(73,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) )
       != ( D @ ( E @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[69]) ).

thf(116,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ is_a_theorem ) )
      | ( G @ is_a_theorem )
      | ~ $true
      | ~ ( G @ ( F @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[100,8]) ).

thf(117,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ is_a_theorem ) )
      | ( G @ is_a_theorem )
      | ~ ( G @ ( F @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[116]) ).

thf(118,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ is_a_theorem )
      | ~ ( A @ ( B @ ( B @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[117:[bind(A,$thf( I )),bind(B,$thf( T )),bind(C,$thf( U )),bind(D,$thf( X )),bind(E,$thf( Y )),bind(F,$thf( I @ ( I @ ( Y @ ( X @ equivalent ) @ equivalent ) @ ( U @ ( T @ equivalent ) @ equivalent ) @ ( T @ ( U @ equivalent ) @ equivalent ) @ ( X @ ( Y @ equivalent ) @ equivalent ) @ equivalent ) )),bind(G,$thf( G ))]]) ).

thf(128,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ is_a_theorem )
      | ~ ( A @ ( B @ ( B @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[118]) ).

thf(1903,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[74,97]) ).

thf(1904,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1903]) ).

thf(1905,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1904:[bind(A,$thf( L )),bind(B,$thf( I )),bind(C,$thf( O )),bind(D,$thf( P )),bind(E,$thf( L )),bind(F,$thf( L @ ( O @ ( P @ equivalent ) @ equivalent ) @ ( I @ equivalent ) )),bind(G,$thf( I )),bind(H,$thf( P @ ( O @ equivalent ) ))]]) ).

thf(2076,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1905]) ).

thf(1939,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[669,97]) ).

thf(1940,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1939]) ).

thf(1941,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1940:[bind(A,$thf( I )),bind(B,$thf( L )),bind(C,$thf( N )),bind(D,$thf( P )),bind(E,$thf( L @ ( N @ ( P @ ( P @ equivalent ) @ equivalent ) @ equivalent ) )),bind(F,$thf( L @ ( I @ equivalent ) )),bind(G,$thf( I )),bind(H,$thf( N ))]]) ).

thf(2036,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1941]) ).

thf(2611,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[2036,97]) ).

thf(2612,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2611]) ).

thf(2613,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( C @ ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2612:[bind(A,$thf( M )),bind(B,$thf( N )),bind(C,$thf( L )),bind(D,$thf( P )),bind(E,$thf( N )),bind(F,$thf( N @ ( M @ equivalent ) @ ( L @ ( M @ equivalent ) @ equivalent ) )),bind(G,$thf( L )),bind(H,$thf( P @ ( P @ equivalent ) ))]]) ).

thf(2645,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( C @ ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2613]) ).

thf(2263,plain,
    ! [B: $i,A: $i] :
      ( ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2251,6]) ).

thf(2264,plain,
    ! [B: $i,A: $i] :
      ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2263]) ).

thf(2292,plain,
    ! [B: $i,A: $i] :
      ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[2264]) ).

thf(1217,plain,
    ( ( e != e )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( c @ ( a @ equivalent ) ) )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a ) ),
    inference(eqfactor_ordered,[status(thm)],[1210]) ).

thf(1219,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != c )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a ) ),
    inference(simp,[status(thm)],[1217]) ).

thf(147,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( A != e )
      | ( ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[125]) ).

thf(148,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( e @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) )
     != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[147]) ).

thf(149,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( e @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) )
       != e )
      | ( ( C @ ( D @ equivalent ) )
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[148]) ).

thf(2567,plain,
    ! [B: $i,A: $i] :
      ( ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) )
       != e )
      | ( A
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[2292]) ).

thf(2568,plain,
    ! [A: $i] :
      ( ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) )
     != e ),
    inference(simp,[status(thm)],[2567]) ).

thf(438,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[419,38]) ).

thf(439,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[438]) ).

thf(440,plain,
    ! [A: $i] : ( A @ ( A @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[439:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( H )),bind(D,$thf( H @ ( H @ equivalent ) )),bind(E,$thf( H )),bind(F,$thf( A ))]]) ).

thf(465,plain,
    ! [A: $i] : ( A @ ( A @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[440]) ).

thf(475,plain,
    ! [A: $i] :
      ( ( ( A @ ( A @ equivalent ) @ is_a_theorem )
       != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[465,6]) ).

thf(476,plain,
    ! [A: $i] :
      ( ( A @ ( A @ equivalent ) @ is_a_theorem )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[475]) ).

thf(498,plain,
    ! [A: $i] :
      ( ( A @ ( A @ equivalent ) )
     != ( e @ ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[476]) ).

thf(512,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[462,40]) ).

thf(513,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( E @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( H @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[512]) ).

thf(514,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( E @ ( D @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( E @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[513:[bind(A,$thf( L )),bind(B,$thf( P )),bind(C,$thf( Q )),bind(D,$thf( R )),bind(E,$thf( R )),bind(F,$thf( R @ ( Q @ equivalent ) @ ( P @ ( Q @ equivalent ) @ equivalent ) @ ( L @ ( P @ equivalent ) @ equivalent ) )),bind(G,$thf( L )),bind(H,$thf( H ))]]) ).

thf(540,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( E @ ( D @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( E @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[514]) ).

thf(2572,plain,
    ! [A: $i] :
      ( ( e != e )
      | ( ( A @ ( A @ equivalent ) )
       != ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[2571]) ).

thf(2573,plain,
    ! [A: $i] :
      ( ( A @ ( A @ equivalent ) )
     != ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) ) ),
    inference(simp,[status(thm)],[2572]) ).

thf(1193,plain,
    ! [B: $i,A: $i] :
      ( ( B != B )
      | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
       != ( A @ ( A @ equivalent ) ) )
      | ( ( B @ ( A @ ( A @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[1191]) ).

thf(1194,plain,
    ! [B: $i,A: $i] :
      ( ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
       != ( A @ ( A @ equivalent ) ) )
      | ( ( B @ ( A @ ( A @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[1193]) ).

thf(1558,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != c )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a ) ),
    inference(simp,[status(thm)],[1555]) ).

thf(2306,plain,
    ( ( a != a )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != c )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b ) ),
    inference(eqfactor_ordered,[status(thm)],[1558]) ).

thf(2309,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != b )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( ( c @ ( a @ equivalent ) )
     != c )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b ) ),
    inference(simp,[status(thm)],[2306]) ).

thf(2311,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) )
     != c )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b ) ),
    inference(simp,[status(thm)],[2309]) ).

thf(1209,plain,
    ( ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[1198]) ).

thf(2600,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( F @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2036,37]) ).

thf(2601,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( F @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2600]) ).

thf(2602,plain,
    ! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2601:[bind(A,$thf( K @ ( Y @ equivalent ) )),bind(B,$thf( W @ ( Y @ ( Y @ equivalent ) @ equivalent ) )),bind(C,$thf( W )),bind(D,$thf( U )),bind(E,$thf( W @ ( Y @ ( Y @ equivalent ) @ equivalent ) @ ( W @ ( U @ ( U @ equivalent ) @ equivalent ) @ equivalent ) )),bind(F,$thf( K )),bind(G,$thf( W )),bind(H,$thf( Y )),bind(I,$thf( Y ))]]) ).

thf(2642,plain,
    ! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2602]) ).

thf(631,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != c )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a )
    | ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b ) ),
    inference(simp,[status(thm)],[629]) ).

thf(731,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[669,39]) ).

thf(732,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[731]) ).

thf(733,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( D @ ( E @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[732:[bind(A,$thf( ZD @ ( ZB @ ( ZA @ equivalent ) @ equivalent ) @ ( ZA @ ( ZB @ equivalent ) @ equivalent ) )),bind(B,$thf( ZD )),bind(C,$thf( ZF )),bind(D,$thf( ZH )),bind(E,$thf( ZD @ ( ZF @ ( ZH @ ( ZH @ equivalent ) @ equivalent ) @ equivalent ) @ ( ZD @ ( ZB @ ( ZA @ equivalent ) @ equivalent ) @ ( ZA @ ( ZB @ equivalent ) @ equivalent ) @ ( ZF @ equivalent ) @ equivalent ) )),bind(F,$thf( ZD )),bind(G,$thf( ZA )),bind(H,$thf( ZB ))]]) ).

thf(758,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( D @ ( E @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[733]) ).

thf(2650,plain,
    ! [B: $i,A: $i] :
      ( ( B != e )
      | ( B
       != ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) ) )
      | ( ( A @ ( A @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[2649]) ).

thf(2651,plain,
    ! [A: $i] :
      ( ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) )
       != e )
      | ( ( A @ ( A @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[2650]) ).

thf(2756,plain,
    ! [A: $i] :
      ( ( e != e )
      | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) )
       != ( A @ ( A @ equivalent ) ) )
      | ( ( A @ ( A @ equivalent ) )
       != e ) ),
    inference(eqfactor_ordered,[status(thm)],[2651]) ).

thf(2757,plain,
    ! [A: $i] :
      ( ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) )
       != ( A @ ( A @ equivalent ) ) )
      | ( ( A @ ( A @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[2756]) ).

thf(62,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[10,38]) ).

thf(63,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[62]) ).

thf(66,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) )
       != ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[63]) ).

thf(1476,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( F @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[1468,37]) ).

thf(1477,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( D @ ( D @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( F @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1476]) ).

thf(1478,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1477:[bind(A,$thf( ZC @ ( ZE @ ( ZD @ equivalent ) @ equivalent ) )),bind(B,$thf( W )),bind(C,$thf( ZC @ ( ZE @ ( ZD @ equivalent ) @ equivalent ) )),bind(D,$thf( ZE )),bind(E,$thf( ZC @ ( ZE @ ( ZD @ equivalent ) @ equivalent ) @ ( ZC @ ( ZE @ ( ZD @ equivalent ) @ equivalent ) @ ( W @ ( W @ equivalent ) @ equivalent ) @ equivalent ) )),bind(F,$thf( ZE )),bind(G,$thf( ZC )),bind(H,$thf( ZD )),bind(I,$thf( ZE ))]]) ).

thf(1508,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1478]) ).

thf(1984,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[1508,97]) ).

thf(1985,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1984]) ).

thf(1986,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1985:[bind(A,$thf( L )),bind(B,$thf( N )),bind(C,$thf( O )),bind(D,$thf( P )),bind(E,$thf( N )),bind(F,$thf( N @ ( P @ ( O @ equivalent ) @ equivalent ) @ ( L @ ( L @ equivalent ) @ equivalent ) )),bind(G,$thf( P )),bind(H,$thf( O ))]]) ).

thf(2051,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1986]) ).

thf(2215,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[2039,97]) ).

thf(2216,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2215]) ).

thf(2217,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( A @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2216:[bind(A,$thf( L )),bind(B,$thf( O @ ( N @ equivalent ) )),bind(C,$thf( M )),bind(D,$thf( M )),bind(E,$thf( M @ ( L @ equivalent ) @ ( O @ ( N @ equivalent ) @ ( L @ equivalent ) @ equivalent ) )),bind(F,$thf( O )),bind(G,$thf( N ))]]) ).

thf(2244,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( A @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2217]) ).

thf(1872,plain,
    ! [B: $i,A: $i] :
      ( ( ( e @ ( B @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) )
       != e )
      | ( A
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[1824]) ).

thf(1873,plain,
    ! [A: $i] :
      ( ( e @ ( A @ ( A @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
     != e ),
    inference(simp,[status(thm)],[1872]) ).

thf(1942,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[1060,97]) ).

thf(1943,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1942]) ).

thf(1944,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( D @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1943:[bind(A,$thf( I )),bind(B,$thf( N )),bind(C,$thf( O )),bind(D,$thf( P )),bind(E,$thf( P @ ( O @ equivalent ) )),bind(F,$thf( P @ ( N @ ( N @ equivalent ) @ equivalent ) @ ( I @ equivalent ) )),bind(G,$thf( I )),bind(H,$thf( O ))]]) ).

thf(2037,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( D @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1944]) ).

thf(105,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( G @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( H @ ( I @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[100,39]) ).

thf(106,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( G @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( H @ ( I @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem ) ),
    inference(simp,[status(thm)],[105]) ).

thf(123,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) )
       != ( F @ ( G @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ ( H @ ( I @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) )
      | ( F @ is_a_theorem ) ),
    inference(simp,[status(thm)],[106]) ).

thf(2597,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != c )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[2595]) ).

thf(2482,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( E @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2409,39]) ).

thf(2483,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( E @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2482]) ).

thf(2484,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ equivalent ) @ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2483:[bind(A,$thf( Y )),bind(B,$thf( Y @ ( ZA @ ( Z @ equivalent ) @ equivalent ) @ ( Z @ ( ZA @ equivalent ) @ equivalent ) )),bind(C,$thf( ZC )),bind(D,$thf( ZC @ ( ZC @ equivalent ) @ ( Y @ ( ZA @ ( Z @ equivalent ) @ equivalent ) @ ( Z @ ( ZA @ equivalent ) @ equivalent ) @ ( Y @ equivalent ) @ equivalent ) )),bind(E,$thf( Y )),bind(F,$thf( Z )),bind(G,$thf( ZA ))]]) ).

thf(2513,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ equivalent ) @ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2484]) ).

thf(64,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[9,38]) ).

thf(65,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[64]) ).

thf(67,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( D @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) )
       != ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[65]) ).

thf(563,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( D @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[467,39]) ).

thf(564,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( D @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ ( G @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[563]) ).

thf(565,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[564:[bind(A,$thf( ZO )),bind(B,$thf( ZP )),bind(C,$thf( Z @ ( ZP @ ( ZO @ equivalent ) @ equivalent ) @ ( ZO @ ( ZP @ equivalent ) @ equivalent ) @ ( ZH @ ( ZG @ equivalent ) @ equivalent ) @ ( ZG @ ( ZH @ equivalent ) @ equivalent ) )),bind(D,$thf( Z )),bind(E,$thf( Z @ ( Z @ ( ZP @ ( ZO @ equivalent ) @ equivalent ) @ ( ZO @ ( ZP @ equivalent ) @ equivalent ) @ ( ZH @ ( ZG @ equivalent ) @ equivalent ) @ ( ZG @ ( ZH @ equivalent ) @ equivalent ) @ equivalent ) )),bind(F,$thf( Z @ ( ZP @ ( ZO @ equivalent ) @ equivalent ) @ ( ZO @ ( ZP @ equivalent ) @ equivalent ) )),bind(G,$thf( ZG )),bind(H,$thf( ZH ))]]) ).

thf(585,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[565]) ).

thf(1218,plain,
    ( ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( c @ ( a @ equivalent ) ) )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != a ) ),
    inference(simp,[status(thm)],[1217]) ).

thf(2336,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( B @ ( A @ equivalent ) @ ( C @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2066,40]) ).

thf(2337,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( B @ ( A @ equivalent ) @ ( C @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2336]) ).

thf(2338,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( A @ ( B @ ( B @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2337:[bind(A,$thf( L )),bind(B,$thf( M )),bind(C,$thf( K )),bind(D,$thf( M @ ( L @ equivalent ) )),bind(E,$thf( M )),bind(F,$thf( K @ ( K @ equivalent ) @ ( L @ equivalent ) )),bind(G,$thf( G ))]]) ).

thf(2354,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( A @ ( B @ ( B @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2338]) ).

thf(1999,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[1294,97]) ).

thf(2000,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1999]) ).

thf(2001,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( D @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2000:[bind(A,$thf( I )),bind(B,$thf( L )),bind(C,$thf( M )),bind(D,$thf( P )),bind(E,$thf( L )),bind(F,$thf( L @ ( P @ ( P @ equivalent ) @ ( M @ equivalent ) @ equivalent ) @ ( I @ equivalent ) )),bind(G,$thf( I )),bind(H,$thf( M ))]]) ).

thf(2056,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( D @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2001]) ).

thf(3398,plain,
    ( ( e != e )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( c @ ( a @ equivalent ) ) )
    | ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b )
    | ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e ) ),
    inference(eqfactor_ordered,[status(thm)],[2590]) ).

thf(3401,plain,
    ( ( ( c @ ( a @ equivalent ) )
     != c )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( ( c @ ( b @ equivalent ) )
     != c )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != b )
    | ( ( c @ ( b @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != e ) ),
    inference(simp,[status(thm)],[3398]) ).

thf(3066,plain,
    ! [A: $i] :
      ( ( e != e )
      | ( ( A @ ( A @ equivalent ) )
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) )
      | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(eqfactor_ordered,[status(thm)],[3065]) ).

thf(3067,plain,
    ! [A: $i] :
      ( ( ( A @ ( A @ equivalent ) )
       != ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) ) )
      | ( ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
       != e ) ),
    inference(simp,[status(thm)],[3066]) ).

thf(1912,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[270,97]) ).

thf(1913,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( H @ equivalent ) @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( F @ ( H @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1912]) ).

thf(1914,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1913:[bind(A,$thf( P )),bind(B,$thf( N )),bind(C,$thf( O )),bind(D,$thf( L )),bind(E,$thf( N )),bind(F,$thf( N @ ( P @ ( O @ equivalent ) @ equivalent ) @ ( L @ ( P @ equivalent ) @ equivalent ) )),bind(G,$thf( L )),bind(H,$thf( O ))]]) ).

thf(2078,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1914]) ).

thf(103,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( e @ ( C @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) )
       != e )
      | ( B
       != ( c @ ( b @ equivalent ) ) )
      | ( A
       != ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[102]) ).

thf(104,plain,
    ! [A: $i] :
      ( ( e @ ( A @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( A @ equivalent ) @ equivalent ) )
     != e ),
    inference(simp,[status(thm)],[103]) ).

thf(1682,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ ( F @ ( H @ ( I @ equivalent ) @ equivalent ) @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( E @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[1294,1604]) ).

thf(1683,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ ( F @ ( H @ ( I @ equivalent ) @ equivalent ) @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1682]) ).

thf(1684,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1683:[bind(A,$thf( U @ ( ZG @ ( ZF @ equivalent ) @ equivalent ) @ ( ZC @ ( ZC @ equivalent ) @ equivalent ) )),bind(B,$thf( U )),bind(C,$thf( ZF @ ( ZG @ equivalent ) )),bind(D,$thf( ZC )),bind(E,$thf( U @ ( U @ ( ZG @ ( ZF @ equivalent ) @ equivalent ) @ ( ZC @ ( ZC @ equivalent ) @ equivalent ) @ ( ZF @ ( ZG @ equivalent ) @ equivalent ) @ equivalent ) )),bind(F,$thf( U )),bind(G,$thf( ZC @ ( ZC @ equivalent ) )),bind(H,$thf( ZG )),bind(I,$thf( ZF ))]]) ).

thf(1721,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1684]) ).

thf(2426,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[2406,97]) ).

thf(2427,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2426]) ).

thf(2428,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( B @ ( B @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2427:[bind(A,$thf( M )),bind(B,$thf( O @ ( N @ equivalent ) )),bind(C,$thf( J )),bind(D,$thf( J )),bind(E,$thf( M @ ( M @ equivalent ) @ ( O @ ( N @ equivalent ) @ ( J @ equivalent ) @ equivalent ) )),bind(F,$thf( O )),bind(G,$thf( N ))]]) ).

thf(2462,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( B @ ( B @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2428]) ).

thf(2271,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem )
       != ( C @ ( D @ ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( C @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2251,39]) ).

thf(2272,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem )
       != ( C @ ( D @ ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( E @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( C @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2271]) ).

thf(2273,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2272:[bind(A,$thf( V @ ( V @ ( ZD @ ( ZC @ equivalent ) @ equivalent ) @ ( ZC @ ( ZD @ equivalent ) @ equivalent ) @ equivalent ) )),bind(B,$thf( T )),bind(C,$thf( V @ ( V @ ( ZD @ ( ZC @ equivalent ) @ equivalent ) @ ( ZC @ ( ZD @ equivalent ) @ equivalent ) @ equivalent ) @ ( T @ ( T @ equivalent ) @ equivalent ) )),bind(D,$thf( V )),bind(E,$thf( ZC )),bind(F,$thf( ZD ))]]) ).

thf(2294,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2273]) ).

thf(1626,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ ( F @ ( H @ ( I @ equivalent ) @ equivalent ) @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( E @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[74,1604]) ).

thf(1627,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( F @ ( G @ ( I @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ ( F @ ( H @ ( I @ equivalent ) @ equivalent ) @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1626]) ).

thf(1628,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1627:[bind(A,$thf( S )),bind(B,$thf( S @ ( ZE @ ( ZD @ equivalent ) @ equivalent ) @ ( Z @ equivalent ) )),bind(C,$thf( Z )),bind(D,$thf( ZD @ ( ZE @ equivalent ) )),bind(E,$thf( S @ ( S @ ( ZE @ ( ZD @ equivalent ) @ equivalent ) @ ( Z @ equivalent ) @ ( ZD @ ( ZE @ equivalent ) @ ( Z @ equivalent ) @ equivalent ) @ equivalent ) )),bind(F,$thf( S )),bind(G,$thf( Z )),bind(H,$thf( ZE )),bind(I,$thf( ZD ))]]) ).

thf(1725,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1628]) ).

thf(36,plain,
    ! [B: $i,A: $i] :
      ( ( ( B @ ( A @ equivalent ) )
       != A )
      | ~ ( A @ is_a_theorem )
      | ( B @ is_a_theorem ) ),
    inference(simp,[status(thm)],[34]) ).

thf(110,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( G @ ( F @ equivalent ) @ is_a_theorem ) )
      | ~ ( F @ is_a_theorem )
      | ~ ( F @ is_a_theorem )
      | ( G @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[100,35]) ).

thf(111,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( A @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( G @ ( F @ equivalent ) @ is_a_theorem ) )
      | ~ ( F @ is_a_theorem )
      | ( G @ is_a_theorem ) ),
    inference(simp,[status(thm)],[110]) ).

thf(112,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ~ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ( C @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[111:[bind(A,$thf( U )),bind(B,$thf( R )),bind(C,$thf( S )),bind(D,$thf( V )),bind(E,$thf( W )),bind(F,$thf( U @ ( W @ ( V @ equivalent ) @ equivalent ) @ ( S @ ( R @ equivalent ) @ equivalent ) @ ( R @ ( S @ equivalent ) @ equivalent ) @ ( V @ ( W @ equivalent ) @ equivalent ) )),bind(G,$thf( U ))]]) ).

thf(126,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ~ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) @ ( D @ ( E @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ( C @ is_a_theorem ) ),
    inference(simp,[status(thm)],[112]) ).

thf(896,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( e @ ( D @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) )
       != e )
      | ( C
       != ( c @ ( b @ equivalent ) ) )
      | ( D
       != ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[149]) ).

thf(897,plain,
    ! [B: $i,A: $i] :
      ( ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ ( A @ ( B @ equivalent ) @ equivalent ) )
     != e ),
    inference(simp,[status(thm)],[896]) ).

thf(1037,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( E @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[1019,39]) ).

thf(1038,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( B @ equivalent ) @ ( C @ ( A @ ( A @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( E @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ is_a_theorem ) ),
    inference(simp,[status(thm)],[1037]) ).

thf(1039,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( D @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1038:[bind(A,$thf( ZG )),bind(B,$thf( U @ ( ZG @ ( ZG @ equivalent ) @ equivalent ) @ ( ZC @ ( ZB @ equivalent ) @ equivalent ) @ ( ZB @ ( ZC @ equivalent ) @ equivalent ) )),bind(C,$thf( U )),bind(D,$thf( U @ ( U @ ( ZG @ ( ZG @ equivalent ) @ equivalent ) @ ( ZC @ ( ZB @ equivalent ) @ equivalent ) @ ( ZB @ ( ZC @ equivalent ) @ equivalent ) @ equivalent ) )),bind(E,$thf( U @ ( ZG @ ( ZG @ equivalent ) @ equivalent ) )),bind(F,$thf( ZB )),bind(G,$thf( ZC ))]]) ).

thf(1065,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( A @ ( D @ ( D @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[1039]) ).

thf(505,plain,
    ! [A: $i] :
      ( ( A != e )
      | ( A
       != ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[498]) ).

thf(506,plain,
    ( ( e @ ( c @ ( b @ equivalent ) @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
   != e ),
    inference(simp,[status(thm)],[505]) ).

thf(257,plain,
    ! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( J @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( J @ equivalent ) @ equivalent ) @ ( H @ ( G @ ( I @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[198,37]) ).

thf(258,plain,
    ! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( D @ ( E @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( H @ ( J @ ( I @ equivalent ) @ equivalent ) @ ( G @ ( J @ equivalent ) @ equivalent ) @ ( H @ ( G @ ( I @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( F @ is_a_theorem ) ),
    inference(simp,[status(thm)],[257]) ).

thf(259,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( A @ ( E @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[258:[bind(A,$thf( ZH @ ( ZE @ ( ZI @ equivalent ) @ equivalent ) )),bind(B,$thf( ZH @ ( ZJ @ ( ZI @ equivalent ) @ equivalent ) )),bind(C,$thf( ZD )),bind(D,$thf( ZE )),bind(E,$thf( ZJ )),bind(F,$thf( ZH @ ( ZJ @ ( ZI @ equivalent ) @ equivalent ) @ ( ZD @ ( ZJ @ ( ZE @ equivalent ) @ equivalent ) @ equivalent ) @ ( ZH @ ( ZE @ ( ZI @ equivalent ) @ equivalent ) @ ( ZD @ equivalent ) @ equivalent ) )),bind(G,$thf( ZE )),bind(H,$thf( ZH )),bind(I,$thf( ZI )),bind(J,$thf( ZJ ))]]) ).

thf(268,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( C @ ( E @ ( D @ equivalent ) @ equivalent ) @ ( A @ ( E @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ ( D @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[259]) ).

thf(92,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[74,38]) ).

thf(93,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[92]) ).

thf(94,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( D @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( C @ ( D @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ equivalent ) )
       != ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( F @ ( G @ equivalent ) @ equivalent ) ) )
      | ( E @ is_a_theorem ) ),
    inference(simp,[status(thm)],[93]) ).

thf(1383,plain,
    ( ( a != a )
    | ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != c )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b ) ),
    inference(eqfactor_ordered,[status(thm)],[1219]) ).

thf(1384,plain,
    ( ( ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) )
     != ( b @ ( a @ equivalent ) ) )
    | ( ( c @ ( a @ equivalent ) )
     != c )
    | ( ( b @ ( a @ equivalent ) )
     != a )
    | ( c != b )
    | ( b != a )
    | ( ( c @ ( a @ equivalent ) )
     != e )
    | ( ( c @ ( b @ equivalent ) )
     != b ) ),
    inference(simp,[status(thm)],[1383]) ).

thf(2668,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ~ $true
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[2642,97]) ).

thf(2669,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( B @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( D @ ( F @ ( G @ equivalent ) @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2668]) ).

thf(2670,plain,
    ! [C: $i,B: $i,A: $i] : ( B @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2669:[bind(A,$thf( K )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I )),bind(E,$thf( I @ ( K @ ( K @ equivalent ) @ equivalent ) )),bind(F,$thf( C )),bind(G,$thf( C ))]]) ).

thf(2699,plain,
    ! [C: $i,B: $i,A: $i] : ( B @ ( B @ ( C @ ( C @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2670]) ).

thf(2541,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2512,40]) ).

thf(2542,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( C @ ( C @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( B @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( E @ ( D @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( E @ ( G @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( G @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2541]) ).

thf(2543,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ equivalent ) @ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2542:[bind(A,$thf( J )),bind(B,$thf( K )),bind(C,$thf( M )),bind(D,$thf( K @ ( J @ equivalent ) )),bind(E,$thf( M @ ( M @ equivalent ) )),bind(F,$thf( K @ ( J @ equivalent ) )),bind(G,$thf( G ))]]) ).

thf(2563,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ equivalent ) @ ( A @ ( C @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2543]) ).

thf(2280,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem )
       != ( D @ ( C @ ( E @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[2251,40]) ).

thf(2281,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem )
       != ( D @ ( C @ ( E @ equivalent ) @ equivalent ) @ is_a_theorem ) )
      | ( D @ ( F @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( F @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2280]) ).

thf(2282,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2281:[bind(A,$thf( N @ ( M @ equivalent ) )),bind(B,$thf( L )),bind(C,$thf( N )),bind(D,$thf( N @ ( M @ equivalent ) @ ( L @ ( L @ equivalent ) @ equivalent ) )),bind(E,$thf( M )),bind(F,$thf( F ))]]) ).

thf(2297,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ equivalent ) @ ( B @ ( B @ equivalent ) @ equivalent ) @ ( A @ ( C @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[2282]) ).

thf(2130,plain,
    ! [A: $i] :
      ( ( ( A @ ( A @ equivalent ) @ is_a_theorem )
       != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) @ is_a_theorem ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[465,1911]) ).

thf(2131,plain,
    ! [A: $i] :
      ( ( A @ ( A @ equivalent ) @ is_a_theorem )
     != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[2130]) ).

thf(2170,plain,
    ! [A: $i] :
      ( ( A @ ( A @ equivalent ) )
     != ( e @ ( c @ ( a @ equivalent ) @ ( b @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( e @ equivalent ) ) ),
    inference(simp,[status(thm)],[2131]) ).

thf(6804,plain,
    $false,
    inference(e,[status(thm)],[2857,9,2072,628,2363,2512,1068,2590,2248,5,379,677,1426,385,550,10,2195,2516,37,1254,2039,2755,125,2571,460,587,619,2456,1911,61,428,74,1604,6,270,661,761,1338,102,714,4172,2589,2409,2596,38,630,429,1824,21,467,3065,97,665,2068,1210,1291,124,339,753,669,1207,2649,1192,1060,13,129,41,73,128,244,2043,2076,2402,674,2645,2292,1219,148,149,2568,545,2293,498,540,672,2573,2358,1194,2311,1209,2642,419,7,39,387,631,758,2757,66,1556,198,462,130,2401,2051,2244,299,35,1873,1208,548,2037,123,2597,2513,95,18,1070,67,16,585,1218,2354,2056,386,465,3401,3067,203,2078,759,104,2591,1721,2406,1508,1558,40,2251,8,235,207,2066,667,1294,2462,2294,2036,1725,36,19,126,897,1056,1065,506,268,94,2651,624,1384,1019,459,200,2699,2563,2297,676,2170,1468,100]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04  % Problem  : LCL103-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.11  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.22/10.50  % Computer : n006.cluster.edu
% 0.22/10.50  % Model    : x86_64 x86_64
% 0.22/10.50  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/10.50  % Memory   : 8046.5625MB
% 0.22/10.50  % OS       : Linux 6.8.0-71-generic
% 0.22/10.50  % CPULimit : 300
% 0.22/10.50  % WCLimit  : 300
% 0.22/10.50  % DateTime : Fri Sep 25 21:51:08 UTC 2026
% 0.26/10.50  % CPUTime  : 
% 0.26/10.50  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.26/11.23  % [INFO] 	 Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ... 
% 1.59/11.49  % [INFO] 	 Parsing done (250ms). 
% 1.75/11.51  % [INFO] 	 Running in sequential loop mode. 
% 2.55/12.09  % [INFO] 	 eprover registered as external prover. 
% 2.55/12.10  % [INFO] 	 Scanning for conjecture ... 
% 2.79/12.23  % [INFO] 	 Found a conjecture (or negated_conjecture) and 3 axioms. Running axiom selection ... 
% 2.79/12.27  % [INFO] 	 Axiom selection finished. Selected 3 axioms (removed 0 axioms). 
% 2.79/12.29  % [INFO] 	 Problem is propositional (TPTP CNF). 
% 2.79/12.29  % [INFO] 	 Type checking passed. 
% 2.93/12.30  % [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 ... 
% 91.86/31.82  % External prover 'e' found a proof!
% 91.86/31.82  % [INFO] 	 Killing All external provers ... 
% 91.86/31.83  % Time passed: 21200ms (effective reasoning time: 20306ms)
% 91.86/31.83  % Axioms used in derivation (3): p_1, condensed_detachment, q_3
% 91.86/31.83  % No. of inferences in proof: 507
% 91.86/31.83  % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p : 21200 ms resp. 20306 ms w/o parsing
% 96.01/32.33  % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 96.01/32.34  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------