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

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

% Computer : n009.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:55 AM UTC 2026

% Result   : Unsatisfiable 72.30s 17.81s
% Output   : Refutation 73.83s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   44
%            Number of leaves      :    3
% Syntax   : Number of formulae    :  557 ( 234 unt;   0 typ;   0 def)
%            Number of atoms       : 1564 ( 554 equ;   0 cnn)
%            Maximal formula atoms :    5 (   2 avg)
%            Number of connectives : 14931 ( 907   ~; 495   |;   0   &;13529   @)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   29 (  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   : 2253 (   0   ^;2253   !;   0   ?;2253   :)

% 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] : ( D @ ( B @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',s_4) ).

thf(8,plain,
    ! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( B @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ ( A @ 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/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).

thf(6,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(7,plain,
    ! [B: $i,A: $i] :
      ( ( B @ is_a_theorem )
      | ~ ( A @ is_a_theorem )
      | ~ ( B @ ( A @ equivalent ) @ is_a_theorem ) ),
    inference(cnf,[status(esa)],[6]) ).

thf(23,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( B @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ ( A @ 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)],[8,7]) ).

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

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

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

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

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

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

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

thf(26,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( B @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ ( A @ 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)],[8,7]) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

thf(666,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] : ( E @ ( E @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( B @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ ( B @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[665:[bind(A,$thf( ZK @ ( ZJ @ equivalent ) @ ( ZI @ ( ZK @ equivalent ) @ ( ZF @ equivalent ) @ equivalent ) @ ( ZI @ ( ZJ @ equivalent ) @ ( ZF @ equivalent ) @ equivalent ) )),bind(B,$thf( ZM )),bind(C,$thf( ZM @ ( ZM @ equivalent ) @ ( ZK @ ( ZJ @ equivalent ) @ ( ZI @ ( ZK @ equivalent ) @ ( ZF @ equivalent ) @ equivalent ) @ ( ZI @ ( ZJ @ equivalent ) @ ( ZF @ equivalent ) @ equivalent ) @ equivalent ) )),bind(D,$thf( ZF )),bind(E,$thf( ZI )),bind(F,$thf( ZJ )),bind(G,$thf( ZK ))]]) ).

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

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

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

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

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

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

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

thf(45,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( D @ ( C @ equivalent ) @ is_a_theorem )
      | ~ ( B @ ( D @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem )
      | ~ ( B @ ( C @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[44:[bind(A,$thf( G )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( L )),bind(E,$thf( J @ ( L @ equivalent ) @ ( G @ equivalent ) )),bind(F,$thf( L @ ( K @ equivalent ) ))]]) ).

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

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

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

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

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

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

thf(1191,plain,
    ! [B: $i,A: $i] :
      ( ~ ( B @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem )
      | ~ ( B @ ( a @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[1190:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( a )),bind(D,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ))]]) ).

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

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

thf(1500,plain,
    ! [A: $i] :
      ~ ( A @ ( A @ equivalent ) @ ( a @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1499:[bind(A,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) )),bind(B,$thf( R )),bind(C,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) )),bind(D,$thf( R @ ( R @ equivalent ) ))]]) ).

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

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

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

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

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

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

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

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

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

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

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

thf(2019,plain,
    ! [A: $i] :
      ~ ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( A @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2018:[bind(A,$thf( E @ ( a @ equivalent ) )),bind(B,$thf( E @ ( a @ equivalent ) )),bind(C,$thf( E ))]]) ).

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

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

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

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

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

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

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

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

thf(669,plain,
    ! [C: $i,B: $i,A: $i] : ( B @ ( A @ equivalent ) @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[668:[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(709,plain,
    ! [C: $i,B: $i,A: $i] : ( B @ ( A @ equivalent ) @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(simp,[status(thm)],[669]) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

thf(111,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( C @ ( E @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( E @ ( D @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( G @ ( H @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( ( I @ ( H @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ) )
      | ( ( G @ ( I @ equivalent ) @ ( F @ equivalent ) )
       != a )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[57,75]) ).

thf(112,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( C @ ( E @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( E @ ( D @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( G @ ( H @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( ( I @ ( H @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ) )
      | ( ( G @ ( I @ equivalent ) @ ( F @ equivalent ) )
       != a ) ),
    inference(simp,[status(thm)],[111]) ).

thf(113,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( F @ ( E @ equivalent ) @ ( D @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ) )
      | ( ( B @ ( A @ equivalent ) @ ( E @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( F @ ( C @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ equivalent ) )
       != a ) ),
    inference(pattern_uni,[status(thm)],[112:[bind(A,$thf( P )),bind(B,$thf( T )),bind(C,$thf( W )),bind(D,$thf( R )),bind(E,$thf( V )),bind(F,$thf( V @ ( R @ equivalent ) @ ( P @ equivalent ) @ ( W @ ( R @ equivalent ) @ ( T @ equivalent ) @ equivalent ) )),bind(G,$thf( P )),bind(H,$thf( W @ ( V @ equivalent ) @ ( T @ equivalent ) )),bind(I,$thf( I ))]]) ).

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

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

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

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

thf(877,plain,
    ( ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) )
   != ( c @ ( b @ equivalent ) ) ),
    inference(simp,[status(thm)],[876]) ).

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

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

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

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

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

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

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

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

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

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

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

thf(1521,plain,
    ! [A: $i] :
      ~ ( c @ ( b @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1520:[bind(A,$thf( a )),bind(B,$thf( S )),bind(C,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) )),bind(D,$thf( c @ ( b @ equivalent ) )),bind(E,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( S @ equivalent ) @ ( a @ equivalent ) )),bind(F,$thf( c @ ( b @ equivalent ) @ ( S @ equivalent ) ))]]) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

thf(2022,plain,
    ! [A: $i] :
      ~ ( A @ ( a @ equivalent ) @ ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2021:[bind(A,$thf( E @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )),bind(B,$thf( E @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )),bind(C,$thf( E ))]]) ).

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

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

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

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

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

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

thf(1497,plain,
    ! [A: $i] :
      ~ ( A @ ( A @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1496:[bind(A,$thf( a )),bind(B,$thf( F )),bind(C,$thf( a )),bind(D,$thf( F @ ( F @ equivalent ) ))]]) ).

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

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

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

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

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

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

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

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

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

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

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

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

thf(3626,plain,
    ! [C: $i,B: $i,A: $i] : ( C @ ( B @ equivalent ) @ ( B @ ( C @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[3625:[bind(A,$thf( ZC @ ( ZB @ equivalent ) @ ( ZB @ ( ZC @ equivalent ) @ ( X @ equivalent ) @ equivalent ) )),bind(B,$thf( ZC )),bind(C,$thf( X )),bind(D,$thf( ZB @ ( ZC @ equivalent ) )),bind(E,$thf( ZC @ ( ZB @ equivalent ) @ ( ZB @ ( ZC @ equivalent ) @ ( X @ equivalent ) @ equivalent ) @ ( X @ equivalent ) )),bind(F,$thf( ZB @ ( ZC @ equivalent ) @ ( X @ equivalent ) )),bind(G,$thf( ZC )),bind(H,$thf( ZC )),bind(I,$thf( ZB ))]]) ).

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

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

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

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

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

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

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

thf(4474,plain,
    ! [A: $i] :
      ~ ( A @ ( a @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4473:[bind(A,$thf( I )),bind(B,$thf( a )),bind(C,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) )),bind(D,$thf( c @ ( b @ equivalent ) )),bind(E,$thf( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( I @ equivalent ) @ ( a @ equivalent ) )),bind(F,$thf( I ))]]) ).

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

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

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

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

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

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

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

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

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

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

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

thf(3978,plain,
    ! [B: $i,A: $i] :
      ( ~ ( B @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem )
      | ~ ( B @ ( a @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[3977:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( a )),bind(D,$thf( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ))]]) ).

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

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

thf(4191,plain,
    ! [B: $i,A: $i] :
      ~ ( A @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4190:[bind(A,$thf( a )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( K @ ( K @ equivalent ) @ ( H @ equivalent ) @ ( a @ equivalent ) )),bind(E,$thf( H ))]]) ).

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

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

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

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

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

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

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

thf(687,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( B @ ( A @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ) )
      | ( ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( A @ equivalent ) )
       != a ) ),
    inference(pattern_uni,[status(thm)],[686:[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(702,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( B @ ( A @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ) )
      | ( ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( A @ equivalent ) )
       != a ) ),
    inference(simp,[status(thm)],[687]) ).

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

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

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

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

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

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

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

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

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

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

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

thf(4274,plain,
    ! [A: $i] :
      ~ ( A @ ( A @ equivalent ) @ ( a @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4273:[bind(A,$thf( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) )),bind(B,$thf( R )),bind(C,$thf( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) )),bind(D,$thf( R @ ( R @ equivalent ) ))]]) ).

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

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

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

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

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

thf(131,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( B @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) )
       != a )
      | ~ ( C @ ( a @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[130:[bind(A,$thf( G )),bind(B,$thf( J )),bind(C,$thf( a )),bind(D,$thf( I )),bind(E,$thf( J @ ( I @ equivalent ) @ ( G @ equivalent ) )),bind(F,$thf( I ))]]) ).

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

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

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

thf(218,plain,
    ! [D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ equivalent ) )
       != a )
      | ~ ( D @ ( a @ equivalent ) @ ( B @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[217:[bind(A,$thf( H )),bind(B,$thf( K )),bind(C,$thf( a )),bind(D,$thf( J )),bind(E,$thf( K @ ( J @ equivalent ) @ ( H @ equivalent ) )),bind(F,$thf( F )),bind(G,$thf( J ))]]) ).

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

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

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

thf(2034,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( C @ ( B @ equivalent ) @ ( C @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
     != a ),
    inference(pattern_uni,[status(thm)],[2033:[bind(A,$thf( G @ ( a @ equivalent ) )),bind(B,$thf( B )),bind(C,$thf( G @ ( a @ equivalent ) )),bind(D,$thf( D )),bind(E,$thf( G ))]]) ).

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

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

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

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

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

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

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

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

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

thf(70,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] : ( A @ ( F @ ( E @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( E @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( F @ ( C @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[69:[bind(A,$thf( P )),bind(B,$thf( T )),bind(C,$thf( W )),bind(D,$thf( R )),bind(E,$thf( V )),bind(F,$thf( V @ ( R @ equivalent ) @ ( P @ equivalent ) @ ( W @ ( R @ equivalent ) @ ( T @ equivalent ) @ equivalent ) )),bind(G,$thf( P )),bind(H,$thf( W @ ( V @ equivalent ) @ ( T @ equivalent ) )),bind(I,$thf( I ))]]) ).

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

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

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

thf(95,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ is_a_theorem )
      | ~ ( A @ ( D @ ( G @ ( F @ equivalent ) @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( F @ ( B @ equivalent ) @ ( C @ equivalent ) @ ( G @ ( B @ equivalent ) @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[94:[bind(A,$thf( Z )),bind(B,$thf( X )),bind(C,$thf( U )),bind(D,$thf( ZA )),bind(E,$thf( ZC )),bind(F,$thf( ZD )),bind(G,$thf( Z @ ( ZD @ ( ZC @ equivalent ) @ ( ZA @ equivalent ) @ equivalent ) @ ( X @ ( Z @ equivalent ) @ ( ZC @ ( U @ equivalent ) @ ( X @ equivalent ) @ ( ZD @ ( U @ equivalent ) @ ( ZA @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )),bind(H,$thf( H ))]]) ).

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

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

thf(115,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( G @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( ( H @ ( G @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ) )
      | ( ( F @ ( H @ equivalent ) @ ( E @ equivalent ) )
       != a )
      | ~ ( B @ ( C @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[114]) ).

thf(116,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( A @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ) )
      | ( ( D @ ( B @ equivalent ) @ ( E @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) )
       != a )
      | ~ ( E @ ( A @ equivalent ) @ ( C @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[115:[bind(A,$thf( I )),bind(B,$thf( L )),bind(C,$thf( C )),bind(D,$thf( K )),bind(E,$thf( L @ ( K @ equivalent ) @ ( I @ equivalent ) )),bind(F,$thf( K )),bind(G,$thf( C )),bind(H,$thf( H ))]]) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

thf(4210,plain,
    ! [B: $i,A: $i] :
      ~ ( A @ ( a @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ ( A @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( B @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4209:[bind(A,$thf( N )),bind(B,$thf( a )),bind(C,$thf( c @ ( b @ equivalent ) )),bind(D,$thf( P )),bind(E,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) )),bind(F,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( P @ equivalent ) @ ( N @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( P @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )),bind(G,$thf( N ))]]) ).

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

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

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

thf(2039,plain,
    ! [C: $i,B: $i,A: $i] : ( A @ ( B @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2038:[bind(A,$thf( G @ ( F @ equivalent ) )),bind(B,$thf( G @ ( F @ equivalent ) )),bind(C,$thf( G )),bind(D,$thf( F ))]]) ).

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

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

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

thf(4318,plain,
    ! [B: $i,A: $i] :
      ~ ( A @ ( a @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( B @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4317:[bind(A,$thf( J )),bind(B,$thf( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) )),bind(C,$thf( K )),bind(D,$thf( K @ ( J @ equivalent ) @ ( K @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )),bind(E,$thf( J ))]]) ).

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

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

thf(79,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( C @ ( E @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( E @ ( D @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( G @ ( H @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( ( I @ ( H @ equivalent ) @ ( G @ ( I @ equivalent ) @ ( F @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ ( a @ equivalent ) ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[57,55]) ).

thf(80,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( C @ ( E @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( E @ ( D @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( G @ ( H @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( ( I @ ( H @ equivalent ) @ ( G @ ( I @ equivalent ) @ ( F @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ ( a @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[79]) ).

thf(81,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ ( F @ ( E @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( E @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( F @ ( C @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ ( a @ equivalent ) ) ),
    inference(pattern_uni,[status(thm)],[80:[bind(A,$thf( P )),bind(B,$thf( T )),bind(C,$thf( W )),bind(D,$thf( R )),bind(E,$thf( V )),bind(F,$thf( V @ ( R @ equivalent ) @ ( P @ equivalent ) @ ( W @ ( R @ equivalent ) @ ( T @ equivalent ) @ equivalent ) )),bind(G,$thf( P )),bind(H,$thf( W @ ( V @ equivalent ) @ ( T @ equivalent ) )),bind(I,$thf( I ))]]) ).

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

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

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

thf(4552,plain,
    ! [A: $i] :
      ~ ( A @ ( a @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4551:[bind(A,$thf( I )),bind(B,$thf( a )),bind(C,$thf( c @ ( b @ equivalent ) )),bind(D,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) )),bind(E,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( I @ equivalent ) @ ( a @ equivalent ) )),bind(F,$thf( I ))]]) ).

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

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

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

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

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

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

thf(2006,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ ( B @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ ( a @ equivalent ) ) ),
    inference(pattern_uni,[status(thm)],[2005:[bind(A,$thf( G @ ( F @ equivalent ) )),bind(B,$thf( G @ ( F @ equivalent ) )),bind(C,$thf( G )),bind(D,$thf( F ))]]) ).

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

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

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

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

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

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

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

thf(4216,plain,
    ! [A: $i] :
      ~ ( A @ ( a @ equivalent ) @ ( A @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4215:[bind(A,$thf( E @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )),bind(B,$thf( E @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )),bind(C,$thf( E ))]]) ).

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

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

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

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

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

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

thf(1454,plain,
    ! [B: $i,A: $i] :
      ~ ( A @ ( a @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( B @ equivalent ) @ ( A @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1453:[bind(A,$thf( N )),bind(B,$thf( a )),bind(C,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) )),bind(D,$thf( P )),bind(E,$thf( c @ ( b @ equivalent ) )),bind(F,$thf( c @ ( b @ equivalent ) @ ( P @ equivalent ) @ ( N @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( P @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )),bind(G,$thf( N ))]]) ).

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

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

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

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

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

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

thf(1444,plain,
    ! [B: $i,A: $i] :
      ~ ( A @ ( a @ equivalent ) @ ( B @ ( B @ equivalent ) @ ( A @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1443:[bind(A,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( K @ ( K @ equivalent ) @ ( H @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )),bind(E,$thf( H ))]]) ).

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

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

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

thf(4306,plain,
    ! [A: $i] :
      ~ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4305:[bind(A,$thf( a )),bind(B,$thf( S )),bind(C,$thf( c @ ( b @ equivalent ) )),bind(D,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) )),bind(E,$thf( c @ ( b @ equivalent ) @ ( S @ equivalent ) @ ( a @ equivalent ) )),bind(F,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( S @ equivalent ) ))]]) ).

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

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

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

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

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

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

thf(4984,plain,
    ! [B: $i,A: $i] :
      ~ ( B @ ( A @ equivalent ) @ ( B @ ( a @ equivalent ) @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4983:[bind(A,$thf( A )),bind(B,$thf( R @ ( a @ equivalent ) )),bind(C,$thf( a )),bind(D,$thf( R )),bind(E,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) )),bind(F,$thf( R ))]]) ).

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

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

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

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

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

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

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

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

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

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

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

thf(2130,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( B @ ( B @ equivalent ) @ ( C @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
     != a ),
    inference(pattern_uni,[status(thm)],[2129:[bind(A,$thf( K @ ( a @ equivalent ) )),bind(B,$thf( I )),bind(C,$thf( I @ ( I @ equivalent ) @ ( K @ ( a @ equivalent ) @ equivalent ) )),bind(D,$thf( D )),bind(E,$thf( K ))]]) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

thf(2065,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( ( A @ ( B @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ) )
      | ( ( C @ ( A @ equivalent ) @ ( C @ ( B @ equivalent ) @ equivalent ) )
       != a ) ),
    inference(pattern_uni,[status(thm)],[2064:[bind(A,$thf( G @ ( F @ equivalent ) )),bind(B,$thf( G @ ( F @ equivalent ) )),bind(C,$thf( G )),bind(D,$thf( F ))]]) ).

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

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

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

thf(4271,plain,
    ! [A: $i] :
      ~ ( A @ ( A @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4270:[bind(A,$thf( a )),bind(B,$thf( F )),bind(C,$thf( a )),bind(D,$thf( F @ ( F @ equivalent ) ))]]) ).

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

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

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

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

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

thf(109,plain,
    ! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( F @ ( E @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( E @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( F @ ( C @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( H @ ( I @ equivalent ) @ ( G @ equivalent ) @ is_a_theorem ) )
      | ( ( J @ ( I @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ) )
      | ( ( H @ ( J @ equivalent ) @ ( G @ equivalent ) )
       != a ) ),
    inference(simp,[status(thm)],[108]) ).

thf(110,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( G @ ( F @ equivalent ) @ ( E @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ) )
      | ( ( C @ ( A @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( F @ ( B @ equivalent ) @ ( D @ equivalent ) @ ( G @ ( B @ equivalent ) @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
       != a ) ),
    inference(pattern_uni,[status(thm)],[109:[bind(A,$thf( W )),bind(B,$thf( X )),bind(C,$thf( U )),bind(D,$thf( Y )),bind(E,$thf( ZA )),bind(F,$thf( ZB )),bind(G,$thf( X @ ( W @ equivalent ) @ ( ZA @ ( U @ equivalent ) @ ( X @ equivalent ) @ ( ZB @ ( U @ equivalent ) @ ( Y @ equivalent ) @ equivalent ) @ equivalent ) )),bind(H,$thf( W )),bind(I,$thf( ZB @ ( ZA @ equivalent ) @ ( Y @ equivalent ) )),bind(J,$thf( J ))]]) ).

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

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

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

thf(654,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != a ),
    inference(pattern_uni,[status(thm)],[653:[bind(A,$thf( a )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( a )),bind(E,$thf( E )),bind(F,$thf( H @ ( H @ equivalent ) ))]]) ).

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

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

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

thf(1884,plain,
    ! [B: $i,A: $i] :
      ~ ( c @ ( b @ equivalent ) @ ( A @ equivalent ) @ ( B @ ( B @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1883:[bind(A,$thf( A )),bind(B,$thf( R @ ( R @ equivalent ) @ ( a @ equivalent ) )),bind(C,$thf( a )),bind(D,$thf( c @ ( b @ equivalent ) )),bind(E,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) )),bind(F,$thf( R ))]]) ).

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

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

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

thf(4287,plain,
    ! [B: $i,A: $i] :
      ~ ( B @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ ( B @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4286:[bind(A,$thf( J @ ( a @ equivalent ) )),bind(B,$thf( H )),bind(C,$thf( H @ ( H @ equivalent ) @ ( J @ ( a @ equivalent ) @ equivalent ) )),bind(D,$thf( J ))]]) ).

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

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

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

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

thf(65,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( C @ ( E @ equivalent ) @ ( B @ equivalent ) @ equivalent ) @ ( E @ ( D @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( B @ 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)],[57,7]) ).

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

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

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

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

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

thf(92,plain,
    ! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( C @ ( F @ ( E @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ ( B @ ( C @ equivalent ) @ ( E @ ( A @ equivalent ) @ ( B @ equivalent ) @ ( F @ ( A @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[91:[bind(A,$thf( X )),bind(B,$thf( V )),bind(C,$thf( S )),bind(D,$thf( Y )),bind(E,$thf( ZA )),bind(F,$thf( ZB )),bind(G,$thf( V @ ( X @ equivalent ) @ ( ZA @ ( S @ equivalent ) @ ( V @ equivalent ) @ ( ZB @ ( S @ equivalent ) @ ( Y @ equivalent ) @ equivalent ) @ equivalent ) )),bind(H,$thf( X @ ( ZB @ ( ZA @ equivalent ) @ ( Y @ equivalent ) @ equivalent ) ))]]) ).

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

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

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

thf(2121,plain,
    ! [B: $i,A: $i] :
      ~ ( B @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ ( B @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2120:[bind(A,$thf( J @ ( a @ equivalent ) )),bind(B,$thf( H )),bind(C,$thf( H @ ( H @ equivalent ) @ ( J @ ( a @ equivalent ) @ equivalent ) )),bind(D,$thf( J ))]]) ).

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

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

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

thf(4213,plain,
    ! [A: $i] :
      ~ ( A @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( A @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4212:[bind(A,$thf( E @ ( a @ equivalent ) )),bind(B,$thf( E @ ( a @ equivalent ) )),bind(C,$thf( E ))]]) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

thf(101,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] : ( A @ ( G @ ( F @ equivalent ) @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( F @ ( B @ equivalent ) @ ( D @ equivalent ) @ ( G @ ( B @ equivalent ) @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[100:[bind(A,$thf( W )),bind(B,$thf( X )),bind(C,$thf( U )),bind(D,$thf( Y )),bind(E,$thf( ZA )),bind(F,$thf( ZB )),bind(G,$thf( X @ ( W @ equivalent ) @ ( ZA @ ( U @ equivalent ) @ ( X @ equivalent ) @ ( ZB @ ( U @ equivalent ) @ ( Y @ equivalent ) @ equivalent ) @ equivalent ) )),bind(H,$thf( W )),bind(I,$thf( ZB @ ( ZA @ equivalent ) @ ( Y @ equivalent ) )),bind(J,$thf( J ))]]) ).

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

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

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

thf(190,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] : ( A @ ( H @ ( G @ equivalent ) @ ( F @ equivalent ) @ equivalent ) @ ( D @ ( A @ equivalent ) @ ( E @ ( D @ equivalent ) @ ( C @ ( E @ equivalent ) @ ( G @ ( B @ equivalent ) @ ( C @ equivalent ) @ ( H @ ( B @ equivalent ) @ ( F @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[189:[bind(A,$thf( ZB )),bind(B,$thf( X )),bind(C,$thf( ZC )),bind(D,$thf( ZA )),bind(E,$thf( ZD )),bind(F,$thf( ZF )),bind(G,$thf( ZG )),bind(H,$thf( ZC @ ( ZB @ equivalent ) @ ( ZA @ ( ZC @ equivalent ) @ ( ZF @ ( X @ equivalent ) @ ( ZA @ equivalent ) @ ( ZG @ ( X @ equivalent ) @ ( ZD @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )),bind(I,$thf( ZB )),bind(J,$thf( ZG @ ( ZF @ equivalent ) @ ( ZD @ equivalent ) )),bind(K,$thf( K ))]]) ).

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

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

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

thf(255,plain,
    ! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] : ( A @ ( I @ ( H @ equivalent ) @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( A @ equivalent ) @ ( F @ ( E @ equivalent ) @ ( D @ ( F @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( H @ ( B @ equivalent ) @ ( C @ equivalent ) @ ( I @ ( B @ equivalent ) @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[254:[bind(A,$thf( ZG )),bind(B,$thf( ZA )),bind(C,$thf( ZD )),bind(D,$thf( ZH )),bind(E,$thf( ZF )),bind(F,$thf( ZI )),bind(G,$thf( ZK )),bind(H,$thf( ZL )),bind(I,$thf( ZH @ ( ZG @ equivalent ) @ ( ZF @ ( ZH @ equivalent ) @ ( ZD @ ( ZF @ equivalent ) @ ( ZK @ ( ZA @ equivalent ) @ ( ZD @ equivalent ) @ ( ZL @ ( ZA @ equivalent ) @ ( ZI @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )),bind(J,$thf( ZG )),bind(K,$thf( ZL @ ( ZK @ equivalent ) @ ( ZI @ equivalent ) )),bind(L,$thf( L ))]]) ).

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

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

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

thf(535,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( B @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != a ),
    inference(pattern_uni,[status(thm)],[534:[bind(A,$thf( a )),bind(B,$thf( K )),bind(C,$thf( L )),bind(D,$thf( L @ ( K @ equivalent ) @ ( a @ equivalent ) )),bind(E,$thf( E )),bind(F,$thf( L @ ( K @ equivalent ) ))]]) ).

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

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

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

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

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

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

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

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

thf(82,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( G @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( ( H @ ( G @ equivalent ) @ ( F @ ( H @ equivalent ) @ ( E @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ ( a @ equivalent ) ) )
      | ~ $true
      | ~ ( B @ ( C @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[32,55]) ).

thf(83,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( G @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( ( H @ ( G @ equivalent ) @ ( F @ ( H @ equivalent ) @ ( E @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ ( a @ equivalent ) ) )
      | ~ ( B @ ( C @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[82]) ).

thf(84,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( B @ ( A @ equivalent ) @ ( D @ ( B @ equivalent ) @ ( E @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ ( a @ equivalent ) ) )
      | ~ ( E @ ( A @ equivalent ) @ ( C @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[83:[bind(A,$thf( I )),bind(B,$thf( L )),bind(C,$thf( C )),bind(D,$thf( K )),bind(E,$thf( L @ ( K @ equivalent ) @ ( I @ equivalent ) )),bind(F,$thf( K )),bind(G,$thf( C )),bind(H,$thf( H ))]]) ).

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

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

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

thf(4315,plain,
    ! [B: $i,A: $i] :
      ~ ( A @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( B @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4314:[bind(A,$thf( J )),bind(B,$thf( a )),bind(C,$thf( K )),bind(D,$thf( K @ ( J @ equivalent ) @ ( K @ ( a @ equivalent ) @ equivalent ) )),bind(E,$thf( J ))]]) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

thf(96,plain,
    ! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( F @ ( E @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( E @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( F @ ( C @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( H @ ( I @ equivalent ) @ ( G @ equivalent ) @ is_a_theorem ) )
      | ( ( J @ ( I @ equivalent ) @ ( H @ ( J @ equivalent ) @ ( G @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ ( a @ equivalent ) ) )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[74,55]) ).

thf(97,plain,
    ! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( F @ ( E @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( E @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( F @ ( C @ equivalent ) @ ( D @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( H @ ( I @ equivalent ) @ ( G @ equivalent ) @ is_a_theorem ) )
      | ( ( J @ ( I @ equivalent ) @ ( H @ ( J @ equivalent ) @ ( G @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ ( a @ equivalent ) ) ) ),
    inference(simp,[status(thm)],[96]) ).

thf(98,plain,
    ! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( A @ ( G @ ( F @ equivalent ) @ ( E @ equivalent ) @ equivalent ) @ ( C @ ( A @ equivalent ) @ ( D @ ( C @ equivalent ) @ ( F @ ( B @ equivalent ) @ ( D @ equivalent ) @ ( G @ ( B @ equivalent ) @ ( E @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
     != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ ( a @ equivalent ) ) ),
    inference(pattern_uni,[status(thm)],[97:[bind(A,$thf( W )),bind(B,$thf( X )),bind(C,$thf( U )),bind(D,$thf( Y )),bind(E,$thf( ZA )),bind(F,$thf( ZB )),bind(G,$thf( X @ ( W @ equivalent ) @ ( ZA @ ( U @ equivalent ) @ ( X @ equivalent ) @ ( ZB @ ( U @ equivalent ) @ ( Y @ equivalent ) @ equivalent ) @ equivalent ) )),bind(H,$thf( W )),bind(I,$thf( ZB @ ( ZA @ equivalent ) @ ( Y @ equivalent ) )),bind(J,$thf( J ))]]) ).

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

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

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

thf(684,plain,
    ! [A: $i] :
      ( ( A @ ( A @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) )
     != a ),
    inference(pattern_uni,[status(thm)],[683:[bind(A,$thf( a )),bind(B,$thf( F )),bind(C,$thf( a )),bind(D,$thf( F @ ( F @ equivalent ) ))]]) ).

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

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

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

thf(2057,plain,
    ! [A: $i] :
      ( ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( a @ equivalent ) @ equivalent ) )
     != a ),
    inference(pattern_uni,[status(thm)],[2056:[bind(A,$thf( E @ ( a @ equivalent ) )),bind(B,$thf( E @ ( a @ equivalent ) )),bind(C,$thf( E ))]]) ).

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

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

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

thf(4194,plain,
    ! [B: $i,A: $i] :
      ~ ( A @ ( a @ equivalent ) @ ( B @ ( B @ equivalent ) @ ( A @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4193:[bind(A,$thf( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( K @ ( K @ equivalent ) @ ( H @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )),bind(E,$thf( H ))]]) ).

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

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

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

thf(4290,plain,
    ! [B: $i,A: $i] :
      ~ ( B @ ( a @ equivalent ) @ ( A @ ( A @ equivalent ) @ ( B @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4289:[bind(A,$thf( J @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )),bind(B,$thf( H )),bind(C,$thf( H @ ( H @ equivalent ) @ ( J @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )),bind(D,$thf( J ))]]) ).

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

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

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

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

thf(232,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( H @ ( a @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( ( E @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( G @ ( E @ equivalent ) @ ( H @ ( G @ equivalent ) @ ( F @ equivalent ) @ equivalent ) @ equivalent ) )
       != a )
      | ~ $true
      | ~ ( B @ ( C @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem ) ),
    inference(paramod_ordered,[status(thm)],[32,225]) ).

thf(233,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( C @ equivalent ) @ ( B @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( H @ ( a @ equivalent ) @ ( F @ equivalent ) @ is_a_theorem ) )
      | ( ( E @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( G @ ( E @ equivalent ) @ ( H @ ( G @ equivalent ) @ ( F @ equivalent ) @ equivalent ) @ equivalent ) )
       != a )
      | ~ ( B @ ( C @ equivalent ) @ ( A @ equivalent ) @ is_a_theorem ) ),
    inference(simp,[status(thm)],[232]) ).

thf(234,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( D @ ( B @ equivalent ) @ ( E @ ( D @ equivalent ) @ ( C @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )
       != a )
      | ~ ( E @ ( a @ equivalent ) @ ( C @ equivalent ) @ is_a_theorem ) ),
    inference(pattern_uni,[status(thm)],[233:[bind(A,$thf( I )),bind(B,$thf( L )),bind(C,$thf( a )),bind(D,$thf( K )),bind(E,$thf( E )),bind(F,$thf( L @ ( K @ equivalent ) @ ( I @ equivalent ) )),bind(G,$thf( G )),bind(H,$thf( K ))]]) ).

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

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

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

thf(2422,plain,
    ! [B: $i,A: $i] :
      ~ ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( B @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2421:[bind(A,$thf( J )),bind(B,$thf( a )),bind(C,$thf( K )),bind(D,$thf( K @ ( J @ equivalent ) @ ( K @ ( a @ equivalent ) @ equivalent ) )),bind(E,$thf( J ))]]) ).

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

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

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

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

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

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

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

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

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

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

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

thf(921,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( B @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ ( A @ ( A @ equivalent ) @ ( C @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != a ),
    inference(pattern_uni,[status(thm)],[920:[bind(A,$thf( O )),bind(B,$thf( a )),bind(C,$thf( P )),bind(D,$thf( N )),bind(E,$thf( P @ ( O @ equivalent ) @ ( N @ ( N @ equivalent ) @ ( P @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )),bind(F,$thf( O ))]]) ).

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

thf(352,plain,
    ! [M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( I @ ( H @ equivalent ) @ ( G @ equivalent ) @ equivalent ) @ ( E @ ( A @ equivalent ) @ ( F @ ( E @ equivalent ) @ ( D @ ( F @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( H @ ( B @ equivalent ) @ ( C @ equivalent ) @ ( I @ ( B @ equivalent ) @ ( G @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( K @ ( L @ equivalent ) @ ( J @ equivalent ) @ is_a_theorem ) )
      | ( M @ ( L @ equivalent ) @ ( K @ ( M @ equivalent ) @ ( J @ equivalent ) @ equivalent ) @ is_a_theorem )
      | ~ $true ),
    inference(paramod_ordered,[status(thm)],[281,32]) ).

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

thf(354,plain,
    ! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] : ( A @ ( J @ ( I @ equivalent ) @ ( H @ equivalent ) @ equivalent ) @ ( F @ ( A @ equivalent ) @ ( G @ ( F @ equivalent ) @ ( E @ ( G @ equivalent ) @ ( D @ ( E @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( I @ ( B @ equivalent ) @ ( C @ equivalent ) @ ( J @ ( B @ equivalent ) @ ( H @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[353:[bind(A,$thf( ZL )),bind(B,$thf( ZD )),bind(C,$thf( ZG )),bind(D,$thf( ZI )),bind(E,$thf( ZM )),bind(F,$thf( ZK )),bind(G,$thf( ZN )),bind(H,$thf( ZP )),bind(I,$thf( ZQ )),bind(J,$thf( ZM @ ( ZL @ equivalent ) @ ( ZK @ ( ZM @ equivalent ) @ ( ZI @ ( ZK @ equivalent ) @ ( ZG @ ( ZI @ equivalent ) @ ( ZP @ ( ZD @ equivalent ) @ ( ZG @ equivalent ) @ ( ZQ @ ( ZD @ equivalent ) @ ( ZN @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) )),bind(K,$thf( ZL )),bind(L,$thf( ZQ @ ( ZP @ equivalent ) @ ( ZN @ equivalent ) )),bind(M,$thf( M ))]]) ).

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

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

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

thf(1853,plain,
    ! [B: $i,A: $i] :
      ~ ( B @ ( A @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( B @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1852:[bind(A,$thf( A )),bind(B,$thf( c @ ( b @ equivalent ) @ ( O @ equivalent ) @ ( a @ equivalent ) )),bind(C,$thf( a )),bind(D,$thf( O )),bind(E,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) )),bind(F,$thf( O ))]]) ).

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

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

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

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

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

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

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

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

thf(660,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( B @ ( A @ equivalent ) @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) )
     != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ ( a @ equivalent ) ) ),
    inference(pattern_uni,[status(thm)],[659:[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(705,plain,
    ! [C: $i,B: $i,A: $i] :
      ( ( B @ ( A @ equivalent ) @ ( C @ ( C @ equivalent ) @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) )
     != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ ( a @ equivalent ) ) ),
    inference(simp,[status(thm)],[660]) ).

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

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

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

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

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

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

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

thf(663,plain,
    ! [B: $i,A: $i] :
      ( ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )
     != a ),
    inference(pattern_uni,[status(thm)],[662:[bind(A,$thf( a )),bind(B,$thf( G )),bind(C,$thf( a )),bind(D,$thf( D )),bind(E,$thf( G @ ( G @ equivalent ) ))]]) ).

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

thf(29,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)],[7]) ).

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

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

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

thf(4657,plain,
    ! [B: $i,A: $i] :
      ~ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( B @ ( B @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4656:[bind(A,$thf( A )),bind(B,$thf( R @ ( R @ equivalent ) @ ( a @ equivalent ) )),bind(C,$thf( a )),bind(D,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) )),bind(E,$thf( c @ ( b @ equivalent ) )),bind(F,$thf( R ))]]) ).

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

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

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

thf(556,plain,
    ! [B: $i,A: $i] :
      ( ( B @ ( A @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )
     != a ),
    inference(pattern_uni,[status(thm)],[555:[bind(A,$thf( a )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( K @ ( J @ equivalent ) @ ( a @ equivalent ) )),bind(E,$thf( K @ ( J @ equivalent ) ))]]) ).

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

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

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

thf(5065,plain,
    ! [B: $i,A: $i] :
      ~ ( B @ ( A @ equivalent ) @ ( B @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[5064:[bind(A,$thf( A )),bind(B,$thf( R @ ( a @ equivalent ) )),bind(C,$thf( a )),bind(D,$thf( R )),bind(E,$thf( c @ ( b @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ equivalent ) )),bind(F,$thf( R ))]]) ).

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

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

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

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

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

thf(2028,plain,
    ! [B: $i,A: $i] :
      ( ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( B @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != a ),
    inference(pattern_uni,[status(thm)],[2027:[bind(A,$thf( F @ ( a @ equivalent ) )),bind(B,$thf( F @ ( a @ equivalent ) )),bind(C,$thf( C )),bind(D,$thf( F ))]]) ).

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

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

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

thf(1441,plain,
    ! [B: $i,A: $i] :
      ~ ( A @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( B @ ( B @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[1440:[bind(A,$thf( a )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( K @ ( K @ equivalent ) @ ( H @ equivalent ) @ ( a @ equivalent ) )),bind(E,$thf( H ))]]) ).

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

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

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

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

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

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

thf(2158,plain,
    ! [B: $i,A: $i] :
      ( ( B @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ equivalent ) @ ( A @ ( A @ equivalent ) @ ( B @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )
     != a ),
    inference(pattern_uni,[status(thm)],[2157:[bind(A,$thf( J @ ( a @ equivalent ) )),bind(B,$thf( H )),bind(C,$thf( H @ ( H @ equivalent ) @ ( J @ ( a @ equivalent ) @ equivalent ) )),bind(D,$thf( J ))]]) ).

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

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

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

thf(4738,plain,
    ! [B: $i,A: $i] :
      ~ ( B @ ( A @ equivalent ) @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( B @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ ( A @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[4737:[bind(A,$thf( A )),bind(B,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( K @ equivalent ) @ ( a @ equivalent ) )),bind(C,$thf( a )),bind(D,$thf( K )),bind(E,$thf( c @ ( b @ equivalent ) )),bind(F,$thf( K ))]]) ).

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

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

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

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

thf(30,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)],[29]) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

thf(2425,plain,
    ! [B: $i,A: $i] :
      ~ ( A @ ( a @ equivalent ) @ ( B @ ( A @ equivalent ) @ ( B @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2424:[bind(A,$thf( J )),bind(B,$thf( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) )),bind(C,$thf( K )),bind(D,$thf( K @ ( J @ equivalent ) @ ( K @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )),bind(E,$thf( J ))]]) ).

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

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

thf(118,plain,
    ! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( D @ ( B @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ ( C @ ( B @ equivalent ) @ ( A @ equivalent ) @ equivalent ) @ is_a_theorem )
       != ( F @ ( G @ equivalent ) @ ( E @ equivalent ) @ is_a_theorem ) )
      | ( ( H @ ( G @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ) )
      | ( ( F @ ( H @ equivalent ) @ ( E @ equivalent ) )
       != a ) ),
    inference(simp,[status(thm)],[117]) ).

thf(119,plain,
    ! [E: $i,D: $i,C: $i,B: $i,A: $i] :
      ( ( ( A @ ( C @ ( E @ equivalent ) @ ( B @ equivalent ) @ equivalent ) )
       != ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) ) )
      | ( ( E @ ( D @ equivalent ) @ ( A @ equivalent ) @ ( C @ ( D @ equivalent ) @ ( B @ equivalent ) @ equivalent ) )
       != a ) ),
    inference(pattern_uni,[status(thm)],[118:[bind(A,$thf( M )),bind(B,$thf( Q )),bind(C,$thf( P )),bind(D,$thf( R )),bind(E,$thf( P @ ( Q @ equivalent ) @ ( M @ equivalent ) )),bind(F,$thf( R @ ( Q @ equivalent ) )),bind(G,$thf( P @ ( R @ equivalent ) @ ( M @ equivalent ) )),bind(H,$thf( H ))]]) ).

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

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

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

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

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

thf(2124,plain,
    ! [B: $i,A: $i] :
      ~ ( B @ ( a @ equivalent ) @ ( A @ ( A @ equivalent ) @ ( B @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) @ equivalent ) @ is_a_theorem ),
    inference(pattern_uni,[status(thm)],[2123:[bind(A,$thf( J @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) )),bind(B,$thf( H )),bind(C,$thf( H @ ( H @ equivalent ) @ ( J @ ( e @ ( c @ equivalent ) @ ( e @ ( b @ equivalent ) @ equivalent ) @ ( c @ ( b @ equivalent ) @ equivalent ) @ ( a @ equivalent ) @ equivalent ) @ equivalent ) )),bind(D,$thf( J ))]]) ).

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

thf(8451,plain,
    $false,
    inference(e,[status(thm)],[2072,6448,2947,1073,5,873,120,878,6463,1808,56,2316,6680,5123,4371,709,3730,2082,2173,702,1191,20,4358,3835,57,5091,2090,646,106,121,937,2324,1714,877,4379,74,6,4370,6464,85,5017,2083,1067,4920,33,1560,1619,137,566,1555,4757,5021,2609,2179,2181,4027,2245,6235,2080,2085,4457,124,225,701,1974,13,4361,1552,2243,134,73,105,2189,2176,4380,32,17,4017,694,22,5121,4677,59,4381,4612,281,875,577,711,4032,641,71,12,1765,86,4369,2624,6461,5303,7,208,6460,4009,103,700,2075,2086,4373,4362,135,241,2069,2506,6687,2171,944,374,1990,123,1551,18,1961,6683,6453,705,5111,707,4366,3940,31,11,72,4695,571,5100,2626,2088,1553,2071,104,2187,2174,55,4834,8,75,3978,58,4774,5119,4014,2255,4357,4597,30,4596,136,2070,1561,2091,4034,4029,4,644,2507,6452,871,122,309,2170,708,2177]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL129-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.08  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.13/0.39  % Computer : n009.cluster.edu
% 0.13/0.39  % Model    : x86_64 x86_64
% 0.13/0.39  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39  % Memory   : 8046.5625MB
% 0.13/0.39  % OS       : Linux 6.8.0-71-generic
% 0.13/0.39  % CPULimit : 300
% 0.13/0.39  % WCLimit  : 300
% 0.13/0.39  % DateTime : Fri Sep 25 21:53:44 UTC 2026
% 0.13/0.39  % CPUTime  : 
% 0.13/0.39  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.88/0.98  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 1.28/1.17  % [INFO] 	 Parsing done (182ms). 
% 1.28/1.18  % [INFO] 	 Running in sequential loop mode. 
% 1.82/1.59  % [INFO] 	 eprover registered as external prover. 
% 2.02/1.60  % [INFO] 	 Scanning for conjecture ... 
% 2.02/1.69  % [INFO] 	 Found a conjecture (or negated_conjecture) and 2 axioms. Running axiom selection ... 
% 2.19/1.72  % [INFO] 	 Axiom selection finished. Selected 2 axioms (removed 0 axioms). 
% 2.19/1.73  % [INFO] 	 Problem is propositional (TPTP CNF). 
% 2.19/1.73  % [INFO] 	 Type checking passed. 
% 2.19/1.73  % [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 ... 
% 72.30/17.80  % External prover 'e' found a proof!
% 72.30/17.80  % [INFO] 	 Killing All external provers ... 
% 72.30/17.80  % Time passed: 17266ms (effective reasoning time: 16613ms)
% 72.30/17.81  % Axioms used in derivation (2): s_4, condensed_detachment
% 72.30/17.81  % No. of inferences in proof: 557
% 72.30/17.81  % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 17266 ms resp. 16613 ms w/o parsing
% 73.83/18.06  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 73.83/18.07  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------