%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LCL195-1 : TPTP v9.3.1. Released v1.1.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 : n018.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:51:07 AM UTC 2026
% Result : Unsatisfiable 113.89s 28.40s
% Output : Refutation 107.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 9
% Syntax : Number of formulae : 796 ( 343 unt; 0 typ; 0 def)
% Number of atoms : 2329 ( 626 equ; 0 cnn)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 11352 (1287 ~; 689 |; 0 &;9376 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 10 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 1751 ( 0 ^;1751 !; 0 ?;1751 :)
% Comments :
%------------------------------------------------------------------------------
thf(theorem_decl,type,
theorem: $i > $o ).
thf(or_decl,type,
or: $i > $i > $i ).
thf(not_decl,type,
not: $i > $i ).
thf(q_decl,type,
q: $i ).
thf(r_decl,type,
r: $i ).
thf(p_decl,type,
p: $i ).
thf(axiom_decl,type,
axiom: $i > $o ).
thf(2,axiom,
! [A: $i] : ( A @ ( A @ ( A @ or ) @ not @ or ) @ axiom ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_2) ).
thf(12,plain,
! [A: $i] : ( A @ ( A @ ( A @ or ) @ not @ or ) @ axiom ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(7,axiom,
! [A: $i] :
( ~ ( A @ axiom )
| ( A @ theorem ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_1) ).
thf(17,plain,
! [A: $i] :
( ~ ( A @ axiom )
| ( A @ theorem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(18,plain,
! [A: $i] :
( ~ ( A @ axiom )
| ( A @ theorem ) ),
inference(cnf,[status(esa)],[17]) ).
thf(116,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ axiom )
!= ( B @ axiom ) )
| ~ $true
| ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[12,18]) ).
thf(117,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ axiom )
!= ( B @ axiom ) )
| ( B @ theorem ) ),
inference(simp,[status(thm)],[116]) ).
thf(118,plain,
! [A: $i] : ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[117:[bind(A,$thf( D )),bind(B,$thf( D @ ( D @ ( D @ or ) @ not @ or ) ))]]) ).
thf(124,plain,
! [A: $i] : ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[118]) ).
thf(3,axiom,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_3) ).
thf(13,plain,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(9,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom )
| ( B @ ( A @ not @ or ) @ theorem ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_3) ).
thf(21,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom )
| ( B @ ( A @ not @ or ) @ theorem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(22,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom )
| ( B @ ( A @ not @ or ) @ theorem ) ),
inference(cnf,[status(esa)],[21]) ).
thf(41,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom )
!= ( E @ ( C @ not @ or ) @ axiom ) )
| ~ ( D @ ( E @ not @ or ) @ theorem )
| ~ $true
| ( D @ ( C @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[13,22]) ).
thf(42,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom )
!= ( E @ ( C @ not @ or ) @ axiom ) )
| ~ ( D @ ( E @ not @ or ) @ theorem )
| ( D @ ( C @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[41]) ).
thf(43,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem )
| ( A @ ( C @ not @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[42:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( G )),bind(D,$thf( D )),bind(E,$thf( G @ ( F @ or ) ))]]) ).
thf(57,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem )
| ( A @ ( C @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[43]) ).
thf(2312,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( B @ ( D @ ( C @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ( B @ ( D @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[124,57]) ).
thf(2313,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( B @ ( D @ ( C @ or ) @ not @ or ) @ theorem ) )
| ( B @ ( D @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2312]) ).
thf(2314,plain,
! [A: $i] : ( A @ ( A @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2313:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A )),bind(D,$thf( A ))]]) ).
thf(6,axiom,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ not @ or ) @ ( B @ ( A @ not @ or ) @ not @ or ) @ axiom ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_6) ).
thf(16,plain,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ not @ or ) @ ( B @ ( A @ not @ or ) @ not @ or ) @ axiom ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(8,axiom,
! [B: $i,A: $i] :
( ~ ( B @ theorem )
| ~ ( A @ ( B @ not @ or ) @ axiom )
| ( A @ theorem ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_2) ).
thf(19,plain,
! [B: $i,A: $i] :
( ~ ( B @ theorem )
| ~ ( A @ ( B @ not @ or ) @ axiom )
| ( A @ theorem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(20,plain,
! [B: $i,A: $i] :
( ~ ( B @ theorem )
| ~ ( A @ ( B @ not @ or ) @ axiom )
| ( A @ theorem ) ),
inference(cnf,[status(esa)],[19]) ).
thf(87,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ not @ or ) @ ( B @ ( A @ not @ or ) @ not @ or ) @ axiom )
!= ( D @ ( E @ not @ or ) @ axiom ) )
| ~ ( E @ theorem )
| ~ $true
| ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[16,20]) ).
thf(88,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ not @ or ) @ ( B @ ( A @ not @ or ) @ not @ or ) @ axiom )
!= ( D @ ( E @ not @ or ) @ axiom ) )
| ~ ( E @ theorem )
| ( D @ theorem ) ),
inference(simp,[status(thm)],[87]) ).
thf(89,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ not @ or ) @ theorem )
| ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[88:[bind(A,$thf( M )),bind(B,$thf( O )),bind(C,$thf( N )),bind(D,$thf( O @ ( N @ or ) @ ( M @ ( N @ or ) @ not @ or ) )),bind(E,$thf( O @ ( M @ not @ or ) ))]]) ).
thf(96,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ not @ or ) @ theorem )
| ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[89]) ).
thf(4,axiom,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ axiom ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_4) ).
thf(14,plain,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ axiom ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(35,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ axiom )
!= ( E @ ( C @ not @ or ) @ axiom ) )
| ~ ( D @ ( E @ not @ or ) @ theorem )
| ~ $true
| ( D @ ( C @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[14,22]) ).
thf(36,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ axiom )
!= ( E @ ( C @ not @ or ) @ axiom ) )
| ~ ( D @ ( E @ not @ or ) @ theorem )
| ( D @ ( C @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[35]) ).
thf(37,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem )
| ( A @ ( B @ ( C @ or ) @ not @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[36:[bind(A,$thf( I )),bind(B,$thf( H )),bind(C,$thf( H @ ( I @ or ) )),bind(D,$thf( D )),bind(E,$thf( I @ ( H @ or ) ))]]) ).
thf(55,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem )
| ( A @ ( B @ ( C @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[37]) ).
thf(26,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom )
!= ( C @ ( D @ not @ or ) @ axiom ) )
| ~ ( D @ theorem )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[13,20]) ).
thf(27,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom )
!= ( C @ ( D @ not @ or ) @ axiom ) )
| ~ ( D @ theorem )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[26]) ).
thf(28,plain,
! [B: $i,A: $i] :
( ~ ( B @ theorem )
| ( B @ ( A @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[27:[bind(A,$thf( F )),bind(B,$thf( E )),bind(C,$thf( F @ ( E @ or ) )),bind(D,$thf( F ))]]) ).
thf(33,plain,
! [B: $i,A: $i] :
( ~ ( B @ theorem )
| ( B @ ( A @ or ) @ theorem ) ),
inference(simp,[status(thm)],[28]) ).
thf(5,axiom,
! [C: $i,B: $i,A: $i] : ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) @ axiom ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_5) ).
thf(15,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) @ axiom ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(58,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) @ axiom )
!= ( D @ ( E @ not @ or ) @ axiom ) )
| ~ ( E @ theorem )
| ~ $true
| ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[15,20]) ).
thf(59,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) @ axiom )
!= ( D @ ( E @ not @ or ) @ axiom ) )
| ~ ( E @ theorem )
| ( D @ theorem ) ),
inference(simp,[status(thm)],[58]) ).
thf(60,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem )
| ( C @ ( B @ or ) @ ( A @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[59:[bind(A,$thf( L )),bind(B,$thf( J )),bind(C,$thf( M )),bind(D,$thf( M @ ( L @ or ) @ ( J @ or ) )),bind(E,$thf( M @ ( J @ or ) @ ( L @ or ) ))]]) ).
thf(64,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem )
| ( C @ ( B @ or ) @ ( A @ or ) @ theorem ) ),
inference(simp,[status(thm)],[60]) ).
thf(1,negated_conjecture,
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
thf(10,plain,
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(11,plain,
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ),
inference(polarity_switch,[status(thm)],[10]) ).
thf(2863,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[64,11]) ).
thf(2864,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2863]) ).
thf(2865,plain,
~ ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2864:[bind(A,$thf( r @ ( q @ not @ or ) @ not )),bind(B,$thf( p @ ( q @ or ) @ not )),bind(C,$thf( p @ ( r @ or ) ))]]) ).
thf(4675,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,2865]) ).
thf(4676,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[4675]) ).
thf(4677,plain,
~ ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4676:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) ))]]) ).
thf(4869,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[55,4677]) ).
thf(4870,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4869]) ).
thf(4871,plain,
~ ( p @ ( r @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4870:[bind(A,$thf( p @ ( r @ or ) )),bind(B,$thf( r )),bind(C,$thf( q @ not ))]]) ).
thf(6400,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[96,4871]) ).
thf(6401,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[6400]) ).
thf(6402,plain,
~ ( p @ ( q @ not @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[6401:[bind(A,$thf( q @ not )),bind(B,$thf( r )),bind(C,$thf( p ))]]) ).
thf(6717,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( q @ not @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,6402]) ).
thf(6718,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( q @ not @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[6717]) ).
thf(6756,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( p @ ( q @ not @ not @ or ) ) ),
inference(simp,[status(thm)],[6718]) ).
thf(374,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,11]) ).
thf(375,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[374]) ).
thf(376,plain,
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[375:[bind(A,$thf( r @ ( q @ not @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) ))]]) ).
thf(449,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[22,376]) ).
thf(450,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[449]) ).
thf(451,plain,
! [A: $i] :
( ~ ( p @ ( r @ or ) @ ( A @ not @ or ) @ theorem )
| ~ ( A @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(pattern_uni,[status(thm)],[450:[bind(A,$thf( p @ ( q @ or ) )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( C ))]]) ).
thf(457,plain,
! [A: $i] :
( ~ ( p @ ( r @ or ) @ ( A @ not @ or ) @ theorem )
| ~ ( A @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[451]) ).
thf(2051,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom )
!= ( C @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( C @ not @ or ) @ theorem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[13,457]) ).
thf(2052,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom )
!= ( C @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( C @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2051]) ).
thf(2053,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ ( A @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2052:[bind(A,$thf( p @ ( q @ or ) )),bind(B,$thf( F )),bind(C,$thf( p @ ( q @ or ) @ ( F @ or ) ))]]) ).
thf(2085,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ ( A @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[2053]) ).
thf(4101,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[55,2085]) ).
thf(4102,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4101]) ).
thf(4103,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( A @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4102:[bind(A,$thf( p @ ( r @ or ) )),bind(B,$thf( p @ ( q @ or ) )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(4176,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( A @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[4103]) ).
thf(4512,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( D @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[64,4176]) ).
thf(4513,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( D @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4512]) ).
thf(4514,plain,
! [A: $i] :
~ ( p @ ( A @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ ( r @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4513:[bind(A,$thf( G @ ( p @ ( q @ or ) @ or ) @ not )),bind(B,$thf( r )),bind(C,$thf( p )),bind(D,$thf( G ))]]) ).
thf(4560,plain,
! [A: $i] :
~ ( p @ ( A @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ ( r @ or ) @ theorem ),
inference(simp,[status(thm)],[4514]) ).
thf(107,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ axiom )
!= ( C @ axiom ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[14,18]) ).
thf(108,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ axiom )
!= ( C @ axiom ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[107]) ).
thf(109,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[108:[bind(A,$thf( J )),bind(B,$thf( I )),bind(C,$thf( J @ ( I @ or ) @ ( I @ ( J @ or ) @ not @ or ) ))]]) ).
thf(126,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[109]) ).
thf(2327,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( C @ ( E @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ( C @ ( E @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[126,57]) ).
thf(2328,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( C @ ( E @ ( D @ or ) @ not @ or ) @ theorem ) )
| ( C @ ( E @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2327]) ).
thf(2329,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2328:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( G @ ( F @ or ) )),bind(D,$thf( G )),bind(E,$thf( F ))]]) ).
thf(2347,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[2329]) ).
thf(50,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[22,11]) ).
thf(51,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[50]) ).
thf(52,plain,
! [A: $i] :
( ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( A @ not @ or ) @ theorem )
| ~ ( A @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(pattern_uni,[status(thm)],[51:[bind(A,$thf( r @ ( q @ not @ or ) )),bind(B,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(C,$thf( C ))]]) ).
thf(54,plain,
! [A: $i] :
( ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( A @ not @ or ) @ theorem )
| ~ ( A @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[52]) ).
thf(69,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom )
!= ( C @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[13,54]) ).
thf(70,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom )
!= ( C @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[69]) ).
thf(71,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ ( A @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[70:[bind(A,$thf( r @ ( q @ not @ or ) )),bind(B,$thf( G )),bind(C,$thf( r @ ( q @ not @ or ) @ ( G @ or ) ))]]) ).
thf(81,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ ( A @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[71]) ).
thf(99,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[22,81]) ).
thf(100,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[99]) ).
thf(101,plain,
! [B: $i,A: $i] :
( ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( A @ not @ or ) @ theorem )
| ~ ( A @ ( r @ ( q @ not @ or ) @ ( B @ or ) @ not @ or ) @ axiom ) ),
inference(pattern_uni,[status(thm)],[100:[bind(A,$thf( r @ ( q @ not @ or ) @ ( E @ or ) )),bind(B,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(C,$thf( C )),bind(D,$thf( E ))]]) ).
thf(102,plain,
! [B: $i,A: $i] :
( ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( A @ not @ or ) @ theorem )
| ~ ( A @ ( r @ ( q @ not @ or ) @ ( B @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[101]) ).
thf(8237,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( r @ ( q @ not @ or ) @ ( D @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[2347,102]) ).
thf(8238,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( r @ ( q @ not @ or ) @ ( D @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[8237]) ).
thf(8239,plain,
! [A: $i] :
~ ( p @ ( q @ or ) @ not @ ( r @ ( q @ not @ or ) @ ( A @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[8238:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( p @ ( q @ or ) @ not )),bind(D,$thf( D ))]]) ).
thf(8288,plain,
! [A: $i] :
~ ( p @ ( q @ or ) @ not @ ( r @ ( q @ not @ or ) @ ( A @ or ) @ not @ or ) @ axiom ),
inference(simp,[status(thm)],[8239]) ).
thf(110,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom )
!= ( C @ axiom ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[13,18]) ).
thf(111,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom )
!= ( C @ axiom ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[110]) ).
thf(112,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[111:[bind(A,$thf( H )),bind(B,$thf( G )),bind(C,$thf( H @ ( G @ or ) @ ( H @ not @ or ) ))]]) ).
thf(122,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[112]) ).
thf(442,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,376]) ).
thf(443,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[442]) ).
thf(444,plain,
~ ( p @ ( r @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[443:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) ))]]) ).
thf(462,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[122,444]) ).
thf(463,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) ),
inference(simp,[status(thm)],[462]) ).
thf(479,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ not @ or ) )
!= ( p @ ( r @ or ) ) ),
inference(simp,[status(thm)],[463]) ).
thf(466,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,444]) ).
thf(467,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[466]) ).
thf(468,plain,
~ ( p @ theorem ),
inference(pattern_uni,[status(thm)],[467:[bind(A,$thf( r )),bind(B,$thf( p ))]]) ).
thf(23,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ axiom )
!= ( C @ ( D @ not @ or ) @ axiom ) )
| ~ ( D @ theorem )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[14,20]) ).
thf(24,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ axiom )
!= ( C @ ( D @ not @ or ) @ axiom ) )
| ~ ( D @ theorem )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[23]) ).
thf(25,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ or ) @ theorem )
| ( B @ ( A @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[24:[bind(A,$thf( H )),bind(B,$thf( G )),bind(C,$thf( H @ ( G @ or ) )),bind(D,$thf( G @ ( H @ or ) ))]]) ).
thf(32,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ or ) @ theorem )
| ( B @ ( A @ or ) @ theorem ) ),
inference(simp,[status(thm)],[25]) ).
thf(324,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[126,32]) ).
thf(325,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[324]) ).
thf(326,plain,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ not @ ( B @ ( A @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[325:[bind(A,$thf( H )),bind(B,$thf( I )),bind(C,$thf( I @ ( H @ or ) )),bind(D,$thf( H @ ( I @ or ) @ not ))]]) ).
thf(352,plain,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ not @ ( B @ ( A @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[326]) ).
thf(2530,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( B @ ( C @ or ) @ theorem ) )
| ~ $true
| ( C @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2314,32]) ).
thf(2531,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( B @ ( C @ or ) @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2530]) ).
thf(2532,plain,
! [A: $i] : ( A @ not @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2531:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ not ))]]) ).
thf(2586,plain,
! [A: $i] : ( A @ not @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2532]) ).
thf(6684,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( q @ not @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,6402]) ).
thf(6685,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( q @ not @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[6684]) ).
thf(6744,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( p @ ( q @ not @ not @ or ) ) ),
inference(simp,[status(thm)],[6685]) ).
thf(2525,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( B @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[2314,457]) ).
thf(2526,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( B @ not @ or ) @ theorem ) )
| ~ ( B @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[2525]) ).
thf(2527,plain,
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[2526:[bind(A,$thf( p @ ( r @ or ) )),bind(B,$thf( p @ ( r @ or ) ))]]) ).
thf(130,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( D @ ( E @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( E @ ( C @ not @ or ) @ axiom )
| ( D @ ( C @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[122,22]) ).
thf(131,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( D @ ( E @ not @ or ) @ theorem ) )
| ~ ( E @ ( C @ not @ or ) @ axiom )
| ( D @ ( C @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[130]) ).
thf(132,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ not @ or ) @ axiom )
| ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[131:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( G @ ( F @ or ) )),bind(E,$thf( G ))]]) ).
thf(149,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ not @ or ) @ axiom )
| ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[132]) ).
thf(11873,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[149,2085]) ).
thf(11874,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[11873]) ).
thf(11875,plain,
! [A: $i] :
~ ( p @ ( p @ ( q @ or ) @ ( A @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[11874:[bind(A,$thf( p @ ( q @ or ) @ ( E @ or ) )),bind(B,$thf( r )),bind(C,$thf( p )),bind(D,$thf( E ))]]) ).
thf(12089,plain,
! [A: $i] :
~ ( p @ ( p @ ( q @ or ) @ ( A @ or ) @ not @ or ) @ axiom ),
inference(simp,[status(thm)],[11875]) ).
thf(493,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,468]) ).
thf(494,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[493]) ).
thf(500,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= p )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[494]) ).
thf(2490,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( B @ ( C @ or ) @ theorem ) )
| ( ( C @ ( B @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,500]) ).
thf(2491,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( B @ ( C @ or ) @ theorem ) )
| ( ( C @ ( B @ or ) )
!= p ) ),
inference(simp,[status(thm)],[2490]) ).
thf(2492,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[2491:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ not ))]]) ).
thf(2590,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= p ),
inference(simp,[status(thm)],[2492]) ).
thf(2016,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ axiom )
!= ( C @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( C @ not @ or ) @ theorem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[14,457]) ).
thf(2017,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ axiom )
!= ( C @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( C @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2016]) ).
thf(2018,plain,
~ ( p @ ( r @ or ) @ ( q @ ( p @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2017:[bind(A,$thf( q )),bind(B,$thf( p )),bind(C,$thf( q @ ( p @ or ) ))]]) ).
thf(2886,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ ( p @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[64,2018]) ).
thf(2887,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ ( p @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2886]) ).
thf(2888,plain,
~ ( p @ ( q @ ( p @ or ) @ not @ or ) @ ( r @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2887:[bind(A,$thf( q @ ( p @ or ) @ not )),bind(B,$thf( r )),bind(C,$thf( p ))]]) ).
thf(3215,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ ( p @ or ) @ not @ or ) @ ( r @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,2888]) ).
thf(3216,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ ( p @ or ) @ not @ or ) @ ( r @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[3215]) ).
thf(3217,plain,
~ ( p @ ( q @ ( p @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[3216:[bind(A,$thf( r )),bind(B,$thf( p @ ( q @ ( p @ or ) @ not @ or ) ))]]) ).
thf(38,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ~ ( D @ ( E @ not @ or ) @ axiom )
| ( D @ theorem )
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[22,20]) ).
thf(39,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ ( D @ ( E @ not @ or ) @ axiom )
| ( D @ theorem )
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[38]) ).
thf(40,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ ( D @ not @ or ) @ not @ or ) @ axiom )
| ( B @ theorem )
| ~ ( C @ ( A @ not @ or ) @ theorem )
| ~ ( A @ ( D @ not @ or ) @ axiom ) ),
inference(pattern_uni,[status(thm)],[39:[bind(A,$thf( H )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( G @ ( H @ not @ or ) ))]]) ).
thf(56,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ ( D @ not @ or ) @ not @ or ) @ axiom )
| ( B @ theorem )
| ~ ( C @ ( A @ not @ or ) @ theorem )
| ~ ( A @ ( D @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[40]) ).
thf(4132,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[64,2085]) ).
thf(4133,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4132]) ).
thf(4134,plain,
! [A: $i] :
~ ( p @ ( p @ ( q @ or ) @ ( A @ or ) @ not @ or ) @ ( r @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4133:[bind(A,$thf( p @ ( q @ or ) @ ( F @ or ) @ not )),bind(B,$thf( r )),bind(C,$thf( p )),bind(D,$thf( F ))]]) ).
thf(4179,plain,
! [A: $i] :
~ ( p @ ( p @ ( q @ or ) @ ( A @ or ) @ not @ or ) @ ( r @ or ) @ theorem ),
inference(simp,[status(thm)],[4134]) ).
thf(7381,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ ( C @ or ) @ not @ or ) @ ( r @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,4179]) ).
thf(7382,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ ( C @ or ) @ not @ or ) @ ( r @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[7381]) ).
thf(7383,plain,
! [A: $i] :
~ ( p @ ( p @ ( q @ or ) @ ( A @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[7382:[bind(A,$thf( r )),bind(B,$thf( p @ ( p @ ( q @ or ) @ ( G @ or ) @ not @ or ) )),bind(C,$thf( G ))]]) ).
thf(7453,plain,
! [A: $i] :
~ ( p @ ( p @ ( q @ or ) @ ( A @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[7383]) ).
thf(7454,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[55,7453]) ).
thf(7455,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[7454]) ).
thf(7456,plain,
! [A: $i] :
~ ( p @ ( A @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[7455:[bind(A,$thf( p )),bind(B,$thf( p @ ( q @ or ) )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(7546,plain,
! [A: $i] :
~ ( p @ ( A @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[7456]) ).
thf(7765,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( C @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,7546]) ).
thf(7766,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( C @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[7765]) ).
thf(7767,plain,
! [A: $i] :
~ ( A @ ( p @ ( q @ or ) @ or ) @ not @ ( p @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[7766:[bind(A,$thf( F @ ( p @ ( q @ or ) @ or ) @ not )),bind(B,$thf( p )),bind(C,$thf( F ))]]) ).
thf(7820,plain,
! [A: $i] :
~ ( A @ ( p @ ( q @ or ) @ or ) @ not @ ( p @ or ) @ theorem ),
inference(simp,[status(thm)],[7767]) ).
thf(8309,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( C @ ( p @ ( q @ or ) @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,7820]) ).
thf(8310,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( C @ ( p @ ( q @ or ) @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[8309]) ).
thf(8311,plain,
! [A: $i] :
~ ( A @ ( p @ ( q @ or ) @ or ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[8310:[bind(A,$thf( p )),bind(B,$thf( F @ ( p @ ( q @ or ) @ or ) @ not )),bind(C,$thf( F ))]]) ).
thf(8385,plain,
! [A: $i] :
~ ( A @ ( p @ ( q @ or ) @ or ) @ not @ theorem ),
inference(simp,[status(thm)],[8311]) ).
thf(6707,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ not @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,6402]) ).
thf(6708,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ not @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[6707]) ).
thf(6709,plain,
~ ( q @ not @ not @ ( p @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[6708:[bind(A,$thf( q @ not @ not )),bind(B,$thf( p ))]]) ).
thf(6776,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ not @ not @ ( p @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,6709]) ).
thf(6777,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ not @ not @ ( p @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[6776]) ).
thf(6778,plain,
~ ( q @ not @ not @ theorem ),
inference(pattern_uni,[status(thm)],[6777:[bind(A,$thf( p )),bind(B,$thf( q @ not @ not ))]]) ).
thf(6862,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ not @ not @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,6778]) ).
thf(6863,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ not @ not @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[6862]) ).
thf(6909,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( q @ not @ not ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[6863]) ).
thf(2655,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2586,33]) ).
thf(2656,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2655]) ).
thf(2657,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2656:[bind(A,$thf( F )),bind(B,$thf( B )),bind(C,$thf( F @ not @ ( F @ or ) ))]]) ).
thf(2729,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2657]) ).
thf(4241,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( E @ ( C @ or ) @ ( D @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2729,64]) ).
thf(4242,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( E @ ( C @ or ) @ ( D @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4241]) ).
thf(4243,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ ( B @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4242:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( F )),bind(D,$thf( A )),bind(E,$thf( F @ not ))]]) ).
thf(4323,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ ( B @ or ) @ theorem ),
inference(simp,[status(thm)],[4243]) ).
thf(7919,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( B @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4323,468]) ).
thf(7920,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( A @ or ) @ ( B @ or ) @ theorem )
!= ( p @ theorem ) ),
inference(simp,[status(thm)],[7919]) ).
thf(8086,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( A @ or ) @ ( B @ or ) )
!= p ),
inference(simp,[status(thm)],[7920]) ).
thf(4900,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[64,4677]) ).
thf(4901,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4900]) ).
thf(4902,plain,
~ ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ ( r @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4901:[bind(A,$thf( r @ ( q @ not @ or ) @ not )),bind(B,$thf( r )),bind(C,$thf( p ))]]) ).
thf(5042,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ ( r @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,4902]) ).
thf(5043,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ ( r @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[5042]) ).
thf(5044,plain,
~ ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[5043:[bind(A,$thf( r )),bind(B,$thf( p @ ( r @ ( q @ not @ or ) @ not @ or ) ))]]) ).
thf(5104,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[55,5044]) ).
thf(5105,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[5104]) ).
thf(5106,plain,
~ ( p @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[5105:[bind(A,$thf( p )),bind(B,$thf( r )),bind(C,$thf( q @ not ))]]) ).
thf(5216,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,5106]) ).
thf(5217,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[5216]) ).
thf(5218,plain,
~ ( q @ not @ ( r @ or ) @ not @ ( p @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[5217:[bind(A,$thf( q @ not @ ( r @ or ) @ not )),bind(B,$thf( p ))]]) ).
thf(5619,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ not @ ( r @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,5218]) ).
thf(5620,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ not @ ( r @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[5619]) ).
thf(5621,plain,
~ ( q @ not @ ( r @ or ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[5620:[bind(A,$thf( p )),bind(B,$thf( q @ not @ ( r @ or ) @ not ))]]) ).
thf(2513,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2314,33]) ).
thf(2514,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2513]) ).
thf(2515,plain,
! [B: $i,A: $i] : ( B @ ( B @ not @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2514:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ ( E @ not @ or ) ))]]) ).
thf(2583,plain,
! [B: $i,A: $i] : ( B @ ( B @ not @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2515]) ).
thf(3836,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ not @ or ) @ ( A @ or ) @ theorem )
!= ( C @ ( E @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ( C @ ( E @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2583,57]) ).
thf(3837,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ not @ or ) @ ( A @ or ) @ theorem )
!= ( C @ ( E @ ( D @ or ) @ not @ or ) @ theorem ) )
| ( C @ ( E @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3836]) ).
thf(3838,plain,
! [B: $i,A: $i] : ( B @ ( B @ not @ or ) @ ( A @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[3837:[bind(A,$thf( H @ ( G @ or ) @ not )),bind(B,$thf( J )),bind(C,$thf( J @ ( J @ not @ or ) )),bind(D,$thf( G )),bind(E,$thf( H ))]]) ).
thf(3961,plain,
! [B: $i,A: $i] : ( B @ ( B @ not @ or ) @ ( A @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[3838]) ).
thf(10850,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ not @ or ) @ ( A @ not @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[3961,32]) ).
thf(10851,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ not @ or ) @ ( A @ not @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[10850]) ).
thf(10852,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ ( B @ not @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[10851:[bind(A,$thf( E )),bind(B,$thf( G )),bind(C,$thf( G @ ( G @ not @ or ) )),bind(D,$thf( E @ not ))]]) ).
thf(11027,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ ( B @ not @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[10852]) ).
thf(11228,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( B @ ( B @ not @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11027,500]) ).
thf(11229,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( B @ ( B @ not @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p ) ),
inference(simp,[status(thm)],[11228]) ).
thf(11230,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ not @ or ) @ ( B @ not @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[11229:[bind(A,$thf( H )),bind(B,$thf( F )),bind(C,$thf( H @ not )),bind(D,$thf( F @ ( F @ not @ or ) ))]]) ).
thf(11491,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ not @ or ) @ ( B @ not @ or ) )
!= p ),
inference(simp,[status(thm)],[11230]) ).
thf(2775,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[64,376]) ).
thf(2776,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2775]) ).
thf(2777,plain,
~ ( p @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2776:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( r )),bind(C,$thf( p ))]]) ).
thf(2953,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,2777]) ).
thf(2954,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2953]) ).
thf(2955,plain,
~ ( p @ ( p @ ( q @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2954:[bind(A,$thf( r )),bind(B,$thf( p @ ( p @ ( q @ or ) @ not @ or ) ))]]) ).
thf(3031,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,2955]) ).
thf(3032,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3031]) ).
thf(3033,plain,
~ ( p @ ( q @ or ) @ not @ ( p @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[3032:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p ))]]) ).
thf(3103,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( q @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,3033]) ).
thf(3104,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( q @ or ) @ not @ ( p @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3103]) ).
thf(3131,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( p @ ( q @ or ) @ not @ ( p @ or ) ) ),
inference(simp,[status(thm)],[3104]) ).
thf(11911,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[149,4677]) ).
thf(11912,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[11911]) ).
thf(11913,plain,
~ ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[11912:[bind(A,$thf( r @ ( q @ not @ or ) )),bind(B,$thf( r )),bind(C,$thf( p ))]]) ).
thf(10759,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ not @ or ) @ ( A @ not @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3961,500]) ).
thf(10760,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ not @ or ) @ ( A @ not @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p ) ),
inference(simp,[status(thm)],[10759]) ).
thf(10761,plain,
! [B: $i,A: $i] :
( ( A @ not @ ( B @ ( B @ not @ or ) @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[10760:[bind(A,$thf( E )),bind(B,$thf( G )),bind(C,$thf( G @ ( G @ not @ or ) )),bind(D,$thf( E @ not ))]]) ).
thf(11010,plain,
! [B: $i,A: $i] :
( ( A @ not @ ( B @ ( B @ not @ or ) @ or ) )
!= p ),
inference(simp,[status(thm)],[10761]) ).
thf(119,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) @ axiom )
!= ( D @ axiom ) )
| ~ $true
| ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[15,18]) ).
thf(120,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) @ axiom )
!= ( D @ axiom ) )
| ( D @ theorem ) ),
inference(simp,[status(thm)],[119]) ).
thf(121,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ ( B @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[120:[bind(A,$thf( N )),bind(B,$thf( L )),bind(C,$thf( O )),bind(D,$thf( O @ ( N @ or ) @ ( L @ or ) @ ( O @ ( L @ or ) @ ( N @ or ) @ not @ or ) ))]]) ).
thf(125,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ ( B @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[121]) ).
thf(4982,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,4871]) ).
thf(4983,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4982]) ).
thf(4984,plain,
~ ( q @ not @ ( r @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4983:[bind(A,$thf( q @ not @ ( r @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) ))]]) ).
thf(5137,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,5044]) ).
thf(5138,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[5137]) ).
thf(5139,plain,
~ ( r @ ( q @ not @ or ) @ not @ ( p @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[5138:[bind(A,$thf( r @ ( q @ not @ or ) @ not )),bind(B,$thf( p ))]]) ).
thf(5277,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( r @ ( q @ not @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,5139]) ).
thf(5278,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( r @ ( q @ not @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[5277]) ).
thf(5279,plain,
~ ( r @ ( q @ not @ or ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[5278:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ not @ or ) @ not ))]]) ).
thf(489,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,468]) ).
thf(490,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[489]) ).
thf(501,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= p )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[490]) ).
thf(595,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( C @ theorem ) )
| ( ( C @ ( B @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[124,501]) ).
thf(596,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( C @ theorem ) )
| ( ( C @ ( B @ or ) )
!= p ) ),
inference(simp,[status(thm)],[595]) ).
thf(597,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( B @ or ) @ not @ or ) @ ( A @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[596:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ ( E @ ( E @ or ) @ not @ or ) ))]]) ).
thf(606,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( B @ or ) @ not @ or ) @ ( A @ or ) )
!= p ),
inference(simp,[status(thm)],[597]) ).
thf(212,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[122,32]) ).
thf(213,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[212]) ).
thf(214,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[213:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( G @ ( F @ or ) )),bind(D,$thf( G @ not ))]]) ).
thf(228,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[214]) ).
thf(61,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) @ axiom )
!= ( F @ ( D @ not @ or ) @ axiom ) )
| ~ ( E @ ( F @ not @ or ) @ theorem )
| ~ $true
| ( E @ ( D @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[15,22]) ).
thf(62,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) @ axiom )
!= ( F @ ( D @ not @ or ) @ axiom ) )
| ~ ( E @ ( F @ not @ or ) @ theorem )
| ( E @ ( D @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[61]) ).
thf(63,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ ( D @ ( C @ or ) @ ( B @ or ) @ not @ or ) @ theorem )
| ( A @ ( D @ ( B @ or ) @ ( C @ or ) @ not @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[62:[bind(A,$thf( M )),bind(B,$thf( K )),bind(C,$thf( N )),bind(D,$thf( N @ ( K @ or ) @ ( M @ or ) )),bind(E,$thf( E )),bind(F,$thf( N @ ( M @ or ) @ ( K @ or ) ))]]) ).
thf(65,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ ( D @ ( C @ or ) @ ( B @ or ) @ not @ or ) @ theorem )
| ( A @ ( D @ ( B @ or ) @ ( C @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[63]) ).
thf(7479,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( D @ ( B @ or ) @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ ( E @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( D @ ( C @ or ) @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[65,7453]) ).
thf(7480,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( D @ ( B @ or ) @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ ( E @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( D @ ( C @ or ) @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[7479]) ).
thf(7481,plain,
! [A: $i] :
~ ( p @ ( p @ ( A @ or ) @ ( q @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[7480:[bind(A,$thf( p )),bind(B,$thf( q )),bind(C,$thf( C )),bind(D,$thf( p )),bind(E,$thf( C ))]]) ).
thf(7548,plain,
! [A: $i] :
~ ( p @ ( p @ ( A @ or ) @ ( q @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[7481]) ).
thf(7859,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( p @ ( C @ or ) @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,7548]) ).
thf(7860,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( p @ ( C @ or ) @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[7859]) ).
thf(7861,plain,
! [A: $i] :
~ ( p @ ( A @ or ) @ ( q @ or ) @ not @ ( p @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[7860:[bind(A,$thf( p @ ( G @ or ) @ ( q @ or ) @ not )),bind(B,$thf( p )),bind(C,$thf( G ))]]) ).
thf(7915,plain,
! [A: $i] :
~ ( p @ ( A @ or ) @ ( q @ or ) @ not @ ( p @ or ) @ theorem ),
inference(simp,[status(thm)],[7861]) ).
thf(8495,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( C @ or ) @ ( q @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,7915]) ).
thf(8496,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( C @ or ) @ ( q @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[8495]) ).
thf(8497,plain,
! [A: $i] :
~ ( p @ ( A @ or ) @ ( q @ or ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[8496:[bind(A,$thf( p )),bind(B,$thf( p @ ( G @ or ) @ ( q @ or ) @ not )),bind(C,$thf( G ))]]) ).
thf(8571,plain,
! [A: $i] :
~ ( p @ ( A @ or ) @ ( q @ or ) @ not @ theorem ),
inference(simp,[status(thm)],[8497]) ).
thf(44,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( E @ ( F @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( F @ ( D @ not @ or ) @ axiom )
| ( E @ ( D @ not @ or ) @ theorem )
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[22,22]) ).
thf(45,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( E @ ( F @ not @ or ) @ theorem ) )
| ~ ( F @ ( D @ not @ or ) @ axiom )
| ( E @ ( D @ not @ or ) @ theorem )
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[44]) ).
thf(46,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ ( D @ not @ or ) @ axiom )
| ( B @ ( D @ not @ or ) @ theorem )
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(pattern_uni,[status(thm)],[45:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( B )),bind(F,$thf( A ))]]) ).
thf(1457,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[55,81]) ).
thf(1458,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ ( D @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( C @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1457]) ).
thf(1459,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( A @ ( r @ ( q @ not @ or ) @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1458:[bind(A,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(B,$thf( r @ ( q @ not @ or ) )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(1503,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( A @ ( r @ ( q @ not @ or ) @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[1459]) ).
thf(1537,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ ( r @ ( q @ not @ or ) @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,1503]) ).
thf(1538,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ ( r @ ( q @ not @ or ) @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1537]) ).
thf(1539,plain,
! [A: $i] :
~ ( A @ ( r @ ( q @ not @ or ) @ or ) @ not @ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1538:[bind(A,$thf( F @ ( r @ ( q @ not @ or ) @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(C,$thf( F ))]]) ).
thf(1557,plain,
! [A: $i] :
~ ( A @ ( r @ ( q @ not @ or ) @ or ) @ not @ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[1539]) ).
thf(1577,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( C @ ( r @ ( q @ not @ or ) @ or ) @ not @ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,1557]) ).
thf(1578,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( C @ ( r @ ( q @ not @ or ) @ or ) @ not @ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1577]) ).
thf(1579,plain,
! [A: $i] :
~ ( A @ ( r @ ( q @ not @ or ) @ or ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1578:[bind(A,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(B,$thf( M @ ( r @ ( q @ not @ or ) @ or ) @ not )),bind(C,$thf( M ))]]) ).
thf(1609,plain,
! [A: $i] :
~ ( A @ ( r @ ( q @ not @ or ) @ or ) @ not @ theorem ),
inference(simp,[status(thm)],[1579]) ).
thf(2235,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ ( p @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,2018]) ).
thf(2236,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ ( p @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2235]) ).
thf(2237,plain,
~ ( q @ ( p @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2236:[bind(A,$thf( q @ ( p @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) ))]]) ).
thf(922,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,500]) ).
thf(923,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[922]) ).
thf(924,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ or ) )
!= p )
| ~ ( B @ theorem ) ),
inference(pattern_uni,[status(thm)],[923:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(3338,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2347,468]) ).
thf(3339,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ theorem ) ),
inference(simp,[status(thm)],[3338]) ).
thf(3431,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ not @ or ) )
!= p ),
inference(simp,[status(thm)],[3339]) ).
thf(3039,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,2955]) ).
thf(3040,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3039]) ).
thf(3052,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( p @ ( p @ ( q @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[3040]) ).
thf(10471,plain,
! [A: $i] :
( ( A != p )
| ( ( A @ not )
!= ( p @ ( q @ or ) @ not ) ) ),
inference(simp,[status(thm)],[3052]) ).
thf(10472,plain,
( ( p @ ( q @ or ) @ not )
!= ( p @ not ) ),
inference(simp,[status(thm)],[10471]) ).
thf(10746,plain,
( ( p @ ( q @ or ) )
!= p ),
inference(simp,[status(thm)],[10472]) ).
thf(3392,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2347,32]) ).
thf(3393,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3392]) ).
thf(3394,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ ( A @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[3393:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( G @ ( F @ or ) )),bind(D,$thf( F @ not ))]]) ).
thf(3453,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ ( A @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[3394]) ).
thf(93,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ not @ or ) @ ( B @ ( A @ not @ or ) @ not @ or ) @ axiom )
!= ( D @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( D @ not @ or ) @ theorem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[16,54]) ).
thf(94,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ not @ or ) @ ( B @ ( A @ not @ or ) @ not @ or ) @ axiom )
!= ( D @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( D @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[93]) ).
thf(95,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( A @ or ) @ ( q @ ( A @ or ) @ not @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[94:[bind(A,$thf( q )),bind(B,$thf( r )),bind(C,$thf( J )),bind(D,$thf( r @ ( J @ or ) @ ( q @ ( J @ or ) @ not @ or ) ))]]) ).
thf(98,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( A @ or ) @ ( q @ ( A @ or ) @ not @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[95]) ).
thf(103,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( D @ or ) @ ( q @ ( D @ or ) @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[22,98]) ).
thf(104,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( D @ or ) @ ( q @ ( D @ or ) @ not @ or ) @ not @ or ) @ theorem ) )
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[103]) ).
thf(105,plain,
! [B: $i,A: $i] :
( ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( A @ not @ or ) @ theorem )
| ~ ( A @ ( r @ ( B @ or ) @ ( q @ ( B @ or ) @ not @ or ) @ not @ or ) @ axiom ) ),
inference(pattern_uni,[status(thm)],[104:[bind(A,$thf( r @ ( J @ or ) @ ( q @ ( J @ or ) @ not @ or ) )),bind(B,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(C,$thf( C )),bind(D,$thf( J ))]]) ).
thf(106,plain,
! [B: $i,A: $i] :
( ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( A @ not @ or ) @ theorem )
| ~ ( A @ ( r @ ( B @ or ) @ ( q @ ( B @ or ) @ not @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[105]) ).
thf(469,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[124,444]) ).
thf(470,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) ),
inference(simp,[status(thm)],[469]) ).
thf(480,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ not @ or ) )
!= ( p @ ( r @ or ) ) ),
inference(simp,[status(thm)],[470]) ).
thf(138,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ ( C @ or ) @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[122,81]) ).
thf(139,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ ( C @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[138]) ).
thf(147,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ not @ or ) )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ ( C @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[139]) ).
thf(3084,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,3033]) ).
thf(3085,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[3084]) ).
thf(3086,plain,
~ ( p @ ( q @ or ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[3085:[bind(A,$thf( p )),bind(B,$thf( p @ ( q @ or ) @ not ))]]) ).
thf(3145,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( q @ or ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,3086]) ).
thf(3146,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( q @ or ) @ not @ theorem ) ),
inference(simp,[status(thm)],[3145]) ).
thf(3189,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( p @ ( q @ or ) @ not ) ),
inference(simp,[status(thm)],[3146]) ).
thf(5224,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,5106]) ).
thf(5225,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[5224]) ).
thf(5250,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( p @ ( q @ not @ ( r @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[5225]) ).
thf(11782,plain,
! [A: $i] :
( ( A != p )
| ( ( A @ not )
!= ( q @ not @ ( r @ or ) @ not ) ) ),
inference(simp,[status(thm)],[5250]) ).
thf(11783,plain,
( ( q @ not @ ( r @ or ) @ not )
!= ( p @ not ) ),
inference(simp,[status(thm)],[11782]) ).
thf(3404,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[2347,54]) ).
thf(3405,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[3404]) ).
thf(3406,plain,
~ ( p @ ( q @ or ) @ not @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[3405:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( p @ ( q @ or ) @ not ))]]) ).
thf(47,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ axiom )
!= ( D @ ( B @ not @ or ) @ axiom ) )
| ~ ( C @ ( D @ not @ or ) @ theorem )
| ~ $true
| ( C @ ( B @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[12,22]) ).
thf(48,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ axiom )
!= ( D @ ( B @ not @ or ) @ axiom ) )
| ~ ( C @ ( D @ not @ or ) @ theorem )
| ( C @ ( B @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[47]) ).
thf(49,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ not @ or ) @ theorem )
| ( A @ ( B @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[48:[bind(A,$thf( F )),bind(B,$thf( F @ ( F @ or ) )),bind(C,$thf( C )),bind(D,$thf( F ))]]) ).
thf(53,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ not @ or ) @ theorem )
| ( A @ ( B @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[49]) ).
thf(958,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( C @ ( D @ not @ or ) @ theorem ) )
| ~ $true
| ( C @ ( D @ ( D @ or ) @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[122,53]) ).
thf(959,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( C @ ( D @ not @ or ) @ theorem ) )
| ( C @ ( D @ ( D @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[958]) ).
thf(960,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[959:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ or ) )),bind(D,$thf( F ))]]) ).
thf(1043,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[960]) ).
thf(66,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ axiom )
!= ( C @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[14,54]) ).
thf(67,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ axiom )
!= ( C @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[66]) ).
thf(68,plain,
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[67:[bind(A,$thf( q @ not )),bind(B,$thf( r )),bind(C,$thf( q @ not @ ( r @ or ) ))]]) ).
thf(83,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[22,68]) ).
thf(84,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[83]) ).
thf(85,plain,
! [A: $i] :
( ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( A @ not @ or ) @ theorem )
| ~ ( A @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(pattern_uni,[status(thm)],[84:[bind(A,$thf( q @ not @ ( r @ or ) )),bind(B,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(C,$thf( C ))]]) ).
thf(86,plain,
! [A: $i] :
( ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( A @ not @ or ) @ theorem )
| ~ ( A @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[85]) ).
thf(5736,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[1043,86]) ).
thf(5737,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[5736]) ).
thf(5738,plain,
~ ( p @ ( r @ or ) @ ( p @ ( r @ or ) @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[5737:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( p @ ( r @ or ) @ ( p @ ( r @ or ) @ or ) ))]]) ).
thf(8255,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( r @ ( q @ not @ or ) @ ( D @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[122,102]) ).
thf(8256,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( r @ ( q @ not @ or ) @ ( D @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[8255]) ).
thf(8257,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ ( A @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[8256:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( p @ ( r @ or ) )),bind(D,$thf( D ))]]) ).
thf(8274,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ ( A @ or ) @ not @ or ) @ axiom ),
inference(simp,[status(thm)],[8257]) ).
thf(4124,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( D @ ( B @ or ) @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ ( E @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( D @ ( C @ or ) @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[65,2085]) ).
thf(4125,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( D @ ( B @ or ) @ ( C @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ ( E @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( D @ ( C @ or ) @ ( B @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4124]) ).
thf(4126,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( p @ ( A @ or ) @ ( q @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4125:[bind(A,$thf( p @ ( r @ or ) )),bind(B,$thf( q )),bind(C,$thf( C )),bind(D,$thf( p )),bind(E,$thf( C ))]]) ).
thf(4178,plain,
! [A: $i] :
~ ( p @ ( r @ or ) @ ( p @ ( A @ or ) @ ( q @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[4126]) ).
thf(4597,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( C @ or ) @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,4178]) ).
thf(4598,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( C @ or ) @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4597]) ).
thf(4599,plain,
! [A: $i] :
~ ( p @ ( A @ or ) @ ( q @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4598:[bind(A,$thf( p @ ( G @ or ) @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( G ))]]) ).
thf(4643,plain,
! [A: $i] :
~ ( p @ ( A @ or ) @ ( q @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[4599]) ).
thf(198,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( B @ ( C @ or ) @ theorem ) )
| ~ $true
| ( C @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[124,32]) ).
thf(199,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( B @ ( C @ or ) @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[198]) ).
thf(200,plain,
! [A: $i] : ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[199:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ ( F @ or ) @ not ))]]) ).
thf(229,plain,
! [A: $i] : ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[200]) ).
thf(371,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[229,33]) ).
thf(372,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[371]) ).
thf(373,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[372:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( H @ ( H @ or ) @ not @ ( H @ or ) ))]]) ).
thf(428,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[373]) ).
thf(11936,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( D @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[149,4176]) ).
thf(11937,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( D @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[11936]) ).
thf(11938,plain,
! [A: $i] :
~ ( p @ ( A @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[11937:[bind(A,$thf( F @ ( p @ ( q @ or ) @ or ) )),bind(B,$thf( r )),bind(C,$thf( p )),bind(D,$thf( F ))]]) ).
thf(12068,plain,
! [A: $i] :
~ ( p @ ( A @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ axiom ),
inference(simp,[status(thm)],[11938]) ).
thf(2669,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,444]) ).
thf(2670,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2669]) ).
thf(2714,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( p @ ( r @ or ) ) ),
inference(simp,[status(thm)],[2670]) ).
thf(4099,plain,
! [A: $i] :
( ( ( A @ not )
!= p )
| ( A != r ) ),
inference(simp,[status(thm)],[2714]) ).
thf(4100,plain,
( ( r @ not )
!= p ),
inference(simp,[status(thm)],[4099]) ).
thf(2380,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ ( p @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,2237]) ).
thf(2381,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ ( p @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2380]) ).
thf(2382,plain,
~ ( q @ ( p @ or ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[2381:[bind(A,$thf( p @ ( r @ or ) )),bind(B,$thf( q @ ( p @ or ) @ not ))]]) ).
thf(383,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[122,33]) ).
thf(384,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[383]) ).
thf(385,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ not @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[384:[bind(A,$thf( H )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ ( H @ or ) @ ( I @ not @ or ) ))]]) ).
thf(422,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ not @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[385]) ).
thf(904,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ not @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( ( E @ ( D @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[422,500]) ).
thf(905,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ not @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( ( E @ ( D @ or ) )
!= p ) ),
inference(simp,[status(thm)],[904]) ).
thf(906,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ or ) @ ( C @ not @ or ) @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[905:[bind(A,$thf( A )),bind(B,$thf( I )),bind(C,$thf( J )),bind(D,$thf( J @ ( I @ or ) @ ( J @ not @ or ) )),bind(E,$thf( A ))]]) ).
thf(942,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ or ) @ ( C @ not @ or ) @ or ) )
!= p ),
inference(simp,[status(thm)],[906]) ).
thf(3080,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( q @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,3033]) ).
thf(3081,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( q @ or ) @ not @ ( p @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3080]) ).
thf(3134,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( p @ ( q @ or ) @ not @ ( p @ or ) ) ),
inference(simp,[status(thm)],[3081]) ).
thf(135,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[122,54]) ).
thf(136,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[135]) ).
thf(137,plain,
~ ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[136:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( p @ ( r @ or ) ))]]) ).
thf(152,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[13,137]) ).
thf(153,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ or ) @ ( A @ not @ or ) @ axiom )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[152]) ).
thf(160,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ or ) @ ( A @ not @ or ) )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[153]) ).
thf(165,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ or ) )
!= ( p @ ( r @ or ) ) )
| ( ( A @ not )
!= ( r @ ( q @ not @ or ) @ not ) ) ),
inference(simp,[status(thm)],[160]) ).
thf(3277,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( q @ ( p @ or ) @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,3217]) ).
thf(3278,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( q @ ( p @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3277]) ).
thf(3330,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( p @ ( q @ ( p @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[3278]) ).
thf(11190,plain,
! [A: $i] :
( ( ( A @ not )
!= p )
| ( A
!= ( q @ ( p @ or ) @ not ) ) ),
inference(simp,[status(thm)],[3330]) ).
thf(11191,plain,
( ( q @ ( p @ or ) @ not @ not )
!= p ),
inference(simp,[status(thm)],[11190]) ).
thf(1214,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( ( C @ ( D @ or ) )
!= p )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,924]) ).
thf(1215,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( ( C @ ( D @ or ) )
!= p )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1214]) ).
thf(1216,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ or ) @ or ) )
!= p )
| ~ ( C @ theorem ) ),
inference(pattern_uni,[status(thm)],[1215:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( F @ ( E @ or ) ))]]) ).
thf(1238,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ or ) @ or ) )
!= p )
| ~ ( C @ theorem ) ),
inference(simp,[status(thm)],[1216]) ).
thf(2145,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[1043,457]) ).
thf(2146,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[2145]) ).
thf(2147,plain,
~ ( p @ ( p @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[2146:[bind(A,$thf( r )),bind(B,$thf( p )),bind(C,$thf( p @ ( p @ or ) ))]]) ).
thf(389,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[228,33]) ).
thf(390,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[389]) ).
thf(391,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[390:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ or ) @ or ) ))]]) ).
thf(424,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[391]) ).
thf(9848,plain,
! [A: $i] :
( ( ( A @ not )
!= p )
| ( A
!= ( q @ not @ not ) ) ),
inference(simp,[status(thm)],[6744]) ).
thf(9849,plain,
( ( q @ not @ not @ not )
!= p ),
inference(simp,[status(thm)],[9848]) ).
thf(189,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ or ) )
!= ( p @ ( r @ or ) ) )
| ( A
!= ( r @ ( q @ not @ or ) ) ) ),
inference(simp,[status(thm)],[165]) ).
thf(192,plain,
! [A: $i] :
( ( r @ ( q @ not @ or ) @ ( A @ or ) )
!= ( p @ ( r @ or ) ) ),
inference(simp,[status(thm)],[189]) ).
thf(658,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ not @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[422,32]) ).
thf(659,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ not @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[658]) ).
thf(660,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( B @ or ) @ ( C @ not @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[659:[bind(A,$thf( A )),bind(B,$thf( I )),bind(C,$thf( J )),bind(D,$thf( J @ ( I @ or ) @ ( J @ not @ or ) )),bind(E,$thf( A ))]]) ).
thf(693,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( B @ or ) @ ( C @ not @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[660]) ).
thf(90,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ not @ or ) @ ( B @ ( A @ not @ or ) @ not @ or ) @ axiom )
!= ( F @ ( D @ not @ or ) @ axiom ) )
| ~ ( E @ ( F @ not @ or ) @ theorem )
| ~ $true
| ( E @ ( D @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[16,22]) ).
thf(91,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ not @ or ) @ ( B @ ( A @ not @ or ) @ not @ or ) @ axiom )
!= ( F @ ( D @ not @ or ) @ axiom ) )
| ~ ( E @ ( F @ not @ or ) @ theorem )
| ( E @ ( D @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[90]) ).
thf(92,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ ( D @ ( C @ or ) @ ( B @ ( C @ or ) @ not @ or ) @ not @ or ) @ theorem )
| ( A @ ( D @ ( B @ not @ or ) @ not @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[91:[bind(A,$thf( N )),bind(B,$thf( P )),bind(C,$thf( O )),bind(D,$thf( P @ ( N @ not @ or ) )),bind(E,$thf( E )),bind(F,$thf( P @ ( O @ or ) @ ( N @ ( O @ or ) @ not @ or ) ))]]) ).
thf(97,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( A @ ( D @ ( C @ or ) @ ( B @ ( C @ or ) @ not @ or ) @ not @ or ) @ theorem )
| ( A @ ( D @ ( B @ not @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[92]) ).
thf(2066,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[126,457]) ).
thf(2067,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[2066]) ).
thf(2068,plain,
~ ( r @ ( p @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[2067:[bind(A,$thf( r )),bind(B,$thf( p )),bind(C,$thf( r @ ( p @ or ) ))]]) ).
thf(3294,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ ( p @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,3217]) ).
thf(3295,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ ( p @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3294]) ).
thf(3296,plain,
~ ( q @ ( p @ or ) @ not @ ( p @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[3295:[bind(A,$thf( q @ ( p @ or ) @ not )),bind(B,$thf( p ))]]) ).
thf(3712,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( q @ ( p @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,3296]) ).
thf(3713,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( q @ ( p @ or ) @ not @ ( p @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3712]) ).
thf(3763,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( q @ ( p @ or ) @ not @ ( p @ or ) ) ),
inference(simp,[status(thm)],[3713]) ).
thf(458,plain,
! [A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[229,444]) ).
thf(459,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) ),
inference(simp,[status(thm)],[458]) ).
thf(478,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) )
!= ( p @ ( r @ or ) ) ),
inference(simp,[status(thm)],[459]) ).
thf(841,plain,
! [A: $i] :
( ( ( A @ ( A @ or ) @ not )
!= p )
| ( A != r ) ),
inference(simp,[status(thm)],[478]) ).
thf(842,plain,
( ( r @ ( r @ or ) @ not )
!= p ),
inference(simp,[status(thm)],[841]) ).
thf(931,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,500]) ).
thf(932,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[931]) ).
thf(933,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ or ) )
!= p )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[932:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(11300,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( B @ ( B @ not @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( C @ ( D @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11027,933]) ).
thf(11301,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( B @ ( B @ not @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( C @ ( D @ or ) )
!= p ) ),
inference(simp,[status(thm)],[11300]) ).
thf(11302,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( A @ ( A @ not @ or ) @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[11301:[bind(A,$thf( H )),bind(B,$thf( F )),bind(C,$thf( H @ not )),bind(D,$thf( F @ ( F @ not @ or ) ))]]) ).
thf(11488,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( A @ ( A @ not @ or ) @ or ) )
!= p ),
inference(simp,[status(thm)],[11302]) ).
thf(2485,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,468]) ).
thf(2486,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ theorem ) ),
inference(simp,[status(thm)],[2485]) ).
thf(2577,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= p ),
inference(simp,[status(thm)],[2486]) ).
thf(2528,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,444]) ).
thf(2529,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2528]) ).
thf(2566,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( p @ ( r @ or ) ) ),
inference(simp,[status(thm)],[2529]) ).
thf(3962,plain,
! [A: $i] :
( ( A != p )
| ( ( A @ not )
!= r ) ),
inference(simp,[status(thm)],[2566]) ).
thf(3963,plain,
( ( p @ not )
!= r ),
inference(simp,[status(thm)],[3962]) ).
thf(2698,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( ( C @ ( B @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,501]) ).
thf(2699,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( ( C @ ( B @ or ) )
!= p ) ),
inference(simp,[status(thm)],[2698]) ).
thf(2700,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ or ) @ ( A @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[2699:[bind(A,$thf( F )),bind(B,$thf( B )),bind(C,$thf( F @ not @ ( F @ or ) ))]]) ).
thf(2724,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ or ) @ ( A @ or ) )
!= p ),
inference(simp,[status(thm)],[2700]) ).
thf(487,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[228,468]) ).
thf(488,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( p @ theorem ) ),
inference(simp,[status(thm)],[487]) ).
thf(499,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ or ) @ or ) )
!= p ),
inference(simp,[status(thm)],[488]) ).
thf(3384,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[2347,457]) ).
thf(3385,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[3384]) ).
thf(3386,plain,
~ ( r @ ( p @ ( q @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[3385:[bind(A,$thf( r )),bind(B,$thf( p )),bind(C,$thf( r ))]]) ).
thf(2638,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( B @ ( D @ ( C @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ( B @ ( D @ not @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2586,57]) ).
thf(2639,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( B @ ( D @ ( C @ or ) @ not @ or ) @ theorem ) )
| ( B @ ( D @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2638]) ).
thf(2640,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ not @ not @ ( B @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2639:[bind(A,$thf( K @ ( J @ or ) @ not )),bind(B,$thf( K @ ( J @ or ) @ not @ not )),bind(C,$thf( J )),bind(D,$thf( K ))]]) ).
thf(2726,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ not @ not @ ( B @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[2640]) ).
thf(337,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[126,54]) ).
thf(338,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[337]) ).
thf(339,plain,
~ ( p @ ( q @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[338:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( p @ ( q @ or ) @ not @ ( p @ ( r @ or ) @ or ) ))]]) ).
thf(190,plain,
! [B: $i,A: $i] :
( ( A != p )
| ( B != r )
| ( ( A @ not )
!= ( r @ ( q @ not @ or ) @ not ) ) ),
inference(simp,[status(thm)],[165]) ).
thf(193,plain,
( ( r @ ( q @ not @ or ) @ not )
!= ( p @ not ) ),
inference(simp,[status(thm)],[190]) ).
thf(464,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[228,444]) ).
thf(465,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( p @ ( r @ or ) @ theorem ) ),
inference(simp,[status(thm)],[464]) ).
thf(476,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ or ) @ or ) )
!= ( p @ ( r @ or ) ) ),
inference(simp,[status(thm)],[465]) ).
thf(4135,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ ( C @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,2085]) ).
thf(4136,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ ( C @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4135]) ).
thf(4137,plain,
! [A: $i] :
~ ( p @ ( q @ or ) @ ( A @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4136:[bind(A,$thf( p @ ( q @ or ) @ ( E @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( E ))]]) ).
thf(4180,plain,
! [A: $i] :
~ ( p @ ( q @ or ) @ ( A @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[4137]) ).
thf(8003,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( B @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4323,32]) ).
thf(8004,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( B @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[8003]) ).
thf(8005,plain,
! [B: $i,A: $i] : ( B @ ( B @ not @ ( A @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[8004:[bind(A,$thf( E )),bind(B,$thf( G )),bind(C,$thf( G @ not @ ( E @ or ) )),bind(D,$thf( G ))]]) ).
thf(8159,plain,
! [B: $i,A: $i] : ( B @ ( B @ not @ ( A @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[8005]) ).
thf(5560,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( r @ ( q @ not @ or ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,5279]) ).
thf(5561,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( r @ ( q @ not @ or ) @ not @ theorem ) ),
inference(simp,[status(thm)],[5560]) ).
thf(5576,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( r @ ( q @ not @ or ) @ not ) ),
inference(simp,[status(thm)],[5561]) ).
thf(7493,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ ( C @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,7453]) ).
thf(7494,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ ( C @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[7493]) ).
thf(7495,plain,
! [A: $i] :
~ ( p @ ( q @ or ) @ ( A @ or ) @ not @ ( p @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[7494:[bind(A,$thf( p @ ( q @ or ) @ ( E @ or ) @ not )),bind(B,$thf( p )),bind(C,$thf( E ))]]) ).
thf(7544,plain,
! [A: $i] :
~ ( p @ ( q @ or ) @ ( A @ or ) @ not @ ( p @ or ) @ theorem ),
inference(simp,[status(thm)],[7495]) ).
thf(485,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[122,468]) ).
thf(486,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ theorem ) ),
inference(simp,[status(thm)],[485]) ).
thf(503,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ not @ or ) )
!= p ),
inference(simp,[status(thm)],[486]) ).
thf(577,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( ( C @ ( B @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[229,501]) ).
thf(578,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( ( C @ ( B @ or ) )
!= p ) ),
inference(simp,[status(thm)],[577]) ).
thf(579,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[578:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( H @ ( H @ or ) @ not @ ( H @ or ) ))]]) ).
thf(605,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ or ) )
!= p ),
inference(simp,[status(thm)],[579]) ).
thf(5760,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[122,86]) ).
thf(5761,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[5760]) ).
thf(5762,plain,
~ ( p @ ( r @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[5761:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( p @ ( r @ or ) ))]]) ).
thf(127,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ~ ( C @ ( D @ not @ or ) @ axiom )
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[122,20]) ).
thf(128,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ ( C @ ( D @ not @ or ) @ axiom )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[127]) ).
thf(129,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ or ) @ ( C @ not @ or ) @ not @ or ) @ axiom )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[128:[bind(A,$thf( H )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ ( H @ or ) @ ( I @ not @ or ) ))]]) ).
thf(148,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ or ) @ ( C @ not @ or ) @ not @ or ) @ axiom )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[129]) ).
thf(156,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ axiom )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[12,137]) ).
thf(157,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ not @ or ) @ axiom )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[156]) ).
thf(161,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ not @ or ) )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[157]) ).
thf(2026,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[122,457]) ).
thf(2027,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[2026]) ).
thf(2028,plain,
~ ( p @ ( p @ ( q @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[2027:[bind(A,$thf( r )),bind(B,$thf( p )),bind(C,$thf( p ))]]) ).
thf(29,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ axiom )
!= ( B @ ( C @ not @ or ) @ axiom ) )
| ~ ( C @ theorem )
| ~ $true
| ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[12,20]) ).
thf(30,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ axiom )
!= ( B @ ( C @ not @ or ) @ axiom ) )
| ~ ( C @ theorem )
| ( B @ theorem ) ),
inference(simp,[status(thm)],[29]) ).
thf(31,plain,
! [A: $i] :
( ~ ( A @ ( A @ or ) @ theorem )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[30:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ ( E @ or ) ))]]) ).
thf(34,plain,
! [A: $i] :
( ~ ( A @ ( A @ or ) @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[31]) ).
thf(174,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( B @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[124,54]) ).
thf(175,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( B @ not @ or ) @ theorem ) )
| ~ ( B @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[174]) ).
thf(176,plain,
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[175:[bind(A,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(B,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ or ) ))]]) ).
thf(3737,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( q @ ( p @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,3296]) ).
thf(3738,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( q @ ( p @ or ) @ not @ ( p @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3737]) ).
thf(3768,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( q @ ( p @ or ) @ not @ ( p @ or ) ) ),
inference(simp,[status(thm)],[3738]) ).
thf(843,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= p )
| ( ( B @ not )
!= r ) ),
inference(simp,[status(thm)],[479]) ).
thf(3345,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2347,500]) ).
thf(3346,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p ) ),
inference(simp,[status(thm)],[3345]) ).
thf(3347,plain,
! [B: $i,A: $i] :
( ( A @ not @ ( B @ ( A @ or ) @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[3346:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( G @ ( F @ or ) )),bind(D,$thf( F @ not ))]]) ).
thf(3458,plain,
! [B: $i,A: $i] :
( ( A @ not @ ( B @ ( A @ or ) @ or ) )
!= p ),
inference(simp,[status(thm)],[3347]) ).
thf(369,plain,
! [A: $i] :
( ( A
!= ( p @ ( r @ or ) ) )
| ( ( A @ ( A @ or ) @ not )
!= ( r @ ( q @ not @ or ) @ not ) ) ),
inference(simp,[status(thm)],[161]) ).
thf(370,plain,
( ( p @ ( r @ or ) @ ( p @ ( r @ or ) @ or ) @ not )
!= ( r @ ( q @ not @ or ) @ not ) ),
inference(simp,[status(thm)],[369]) ).
thf(640,plain,
( ( p @ ( r @ or ) @ ( p @ ( r @ or ) @ or ) )
!= ( r @ ( q @ not @ or ) ) ),
inference(simp,[status(thm)],[370]) ).
thf(641,plain,
( ( ( p @ ( r @ or ) )
!= r )
| ( ( p @ ( r @ or ) )
!= ( q @ not ) ) ),
inference(simp,[status(thm)],[640]) ).
thf(9982,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( D @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( D @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[125,54]) ).
thf(9983,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( D @ not @ or ) @ theorem ) )
| ~ ( D @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[9982]) ).
thf(9984,plain,
~ ( p @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[9983:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( r )),bind(C,$thf( p )),bind(D,$thf( p @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ or ) ))]]) ).
thf(483,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[126,468]) ).
thf(484,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ theorem ) ),
inference(simp,[status(thm)],[483]) ).
thf(498,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) )
!= p ),
inference(simp,[status(thm)],[484]) ).
thf(3302,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( q @ ( p @ or ) @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,3217]) ).
thf(3303,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( q @ ( p @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3302]) ).
thf(3324,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( p @ ( q @ ( p @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[3303]) ).
thf(11037,plain,
! [A: $i] :
( ( A != p )
| ( ( A @ not )
!= ( q @ ( p @ or ) @ not ) ) ),
inference(simp,[status(thm)],[3324]) ).
thf(11038,plain,
( ( q @ ( p @ or ) @ not )
!= ( p @ not ) ),
inference(simp,[status(thm)],[11037]) ).
thf(514,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[352,468]) ).
thf(515,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ or ) @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( p @ theorem ) ),
inference(simp,[status(thm)],[514]) ).
thf(540,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ or ) @ not @ ( B @ ( A @ or ) @ or ) )
!= p ),
inference(simp,[status(thm)],[515]) ).
thf(140,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( C @ or ) @ ( q @ ( C @ or ) @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[122,98]) ).
thf(141,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( C @ or ) @ ( q @ ( C @ or ) @ not @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[140]) ).
thf(144,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ not @ or ) )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( C @ or ) @ ( q @ ( C @ or ) @ not @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[141]) ).
thf(592,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,501]) ).
thf(593,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[592]) ).
thf(594,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) )
!= p )
| ~ ( C @ theorem ) ),
inference(pattern_uni,[status(thm)],[593:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( F @ ( E @ or ) ))]]) ).
thf(604,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) )
!= p )
| ~ ( C @ theorem ) ),
inference(simp,[status(thm)],[594]) ).
thf(6858,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( q @ not @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,6778]) ).
thf(6859,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( q @ not @ not @ theorem ) ),
inference(simp,[status(thm)],[6858]) ).
thf(6920,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( q @ not @ not ) ),
inference(simp,[status(thm)],[6859]) ).
thf(3387,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( E @ ( C @ or ) @ ( D @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2347,64]) ).
thf(3388,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( E @ ( C @ or ) @ ( D @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3387]) ).
thf(3389,plain,
! [B: $i,A: $i] : ( A @ ( B @ not @ or ) @ ( B @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[3388:[bind(A,$thf( F )),bind(B,$thf( B )),bind(C,$thf( F )),bind(D,$thf( F @ not )),bind(E,$thf( B ))]]) ).
thf(3468,plain,
! [B: $i,A: $i] : ( A @ ( B @ not @ or ) @ ( B @ or ) @ theorem ),
inference(simp,[status(thm)],[3389]) ).
thf(3014,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,2955]) ).
thf(3015,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( p @ ( q @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3014]) ).
thf(3066,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( p @ ( p @ ( q @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[3015]) ).
thf(5387,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( C @ ( D @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3453,933]) ).
thf(5388,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( C @ ( D @ or ) )
!= p ) ),
inference(simp,[status(thm)],[5387]) ).
thf(5389,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( A @ ( B @ or ) @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[5388:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( G @ not )),bind(D,$thf( F @ ( G @ or ) ))]]) ).
thf(5511,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( A @ ( B @ or ) @ or ) )
!= p ),
inference(simp,[status(thm)],[5389]) ).
thf(583,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[122,501]) ).
thf(584,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p ) ),
inference(simp,[status(thm)],[583]) ).
thf(585,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ or ) @ ( C @ not @ or ) @ ( A @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[584:[bind(A,$thf( H )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ ( H @ or ) @ ( I @ not @ or ) ))]]) ).
thf(609,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ or ) @ ( C @ not @ or ) @ ( A @ or ) )
!= p ),
inference(simp,[status(thm)],[585]) ).
thf(10752,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ not @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3961,468]) ).
thf(10753,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ not @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ theorem ) ),
inference(simp,[status(thm)],[10752]) ).
thf(10942,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ not @ or ) @ ( A @ not @ or ) )
!= p ),
inference(simp,[status(thm)],[10753]) ).
thf(3167,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( q @ or ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,3086]) ).
thf(3168,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( q @ or ) @ not @ theorem ) ),
inference(simp,[status(thm)],[3167]) ).
thf(3192,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( p @ ( q @ or ) @ not ) ),
inference(simp,[status(thm)],[3168]) ).
thf(2540,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( B @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[2314,54]) ).
thf(2541,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( B @ not @ or ) @ theorem ) )
| ~ ( B @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[2540]) ).
thf(2542,plain,
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[2541:[bind(A,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(B,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) ))]]) ).
thf(5826,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( q @ not @ ( r @ or ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,5621]) ).
thf(5827,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( q @ not @ ( r @ or ) @ not @ theorem ) ),
inference(simp,[status(thm)],[5826]) ).
thf(5863,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( q @ not @ ( r @ or ) @ not ) ),
inference(simp,[status(thm)],[5827]) ).
thf(10145,plain,
! [A: $i] :
( ( A != p )
| ( ( A @ not )
!= ( q @ not @ not ) ) ),
inference(simp,[status(thm)],[6756]) ).
thf(10146,plain,
( ( q @ not @ not )
!= ( p @ not ) ),
inference(simp,[status(thm)],[10145]) ).
thf(10147,plain,
( ( q @ not )
!= p ),
inference(simp,[status(thm)],[10146]) ).
thf(3879,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ not @ or ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2583,32]) ).
thf(3880,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ not @ or ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[3879]) ).
thf(3881,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ not @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[3880:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( F @ ( F @ not @ or ) )),bind(D,$thf( A ))]]) ).
thf(3953,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ not @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[3881]) ).
thf(75,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) @ axiom )
!= ( D @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( D @ not @ or ) @ theorem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15,54]) ).
thf(76,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) @ axiom )
!= ( D @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( D @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[75]) ).
thf(80,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) )
!= ( D @ ( r @ ( q @ not @ or ) @ not @ or ) ) )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( D @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[76]) ).
thf(218,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ ( C @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,81]) ).
thf(219,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ ( C @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[218]) ).
thf(220,plain,
! [A: $i] :
~ ( r @ ( q @ not @ or ) @ ( A @ or ) @ not @ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[219:[bind(A,$thf( r @ ( q @ not @ or ) @ ( E @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(C,$thf( E ))]]) ).
thf(231,plain,
! [A: $i] :
~ ( r @ ( q @ not @ or ) @ ( A @ or ) @ not @ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[220]) ).
thf(377,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( r @ ( q @ not @ or ) @ ( C @ or ) @ not @ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,231]) ).
thf(378,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( r @ ( q @ not @ or ) @ ( C @ or ) @ not @ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[377]) ).
thf(379,plain,
! [A: $i] :
~ ( r @ ( q @ not @ or ) @ ( A @ or ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[378:[bind(A,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(B,$thf( r @ ( q @ not @ or ) @ ( L @ or ) @ not )),bind(C,$thf( L ))]]) ).
thf(431,plain,
! [A: $i] :
~ ( r @ ( q @ not @ or ) @ ( A @ or ) @ not @ theorem ),
inference(simp,[status(thm)],[379]) ).
thf(395,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[124,33]) ).
thf(396,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[395]) ).
thf(397,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ not @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[396:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ ( E @ ( E @ or ) @ not @ or ) ))]]) ).
thf(426,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ not @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[397]) ).
thf(10748,plain,
! [A: $i] :
( ( ( A @ not )
!= p )
| ( A
!= ( p @ ( q @ or ) @ not ) ) ),
inference(simp,[status(thm)],[3066]) ).
thf(10749,plain,
( ( p @ ( q @ or ) @ not @ not )
!= p ),
inference(simp,[status(thm)],[10748]) ).
thf(158,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) @ axiom )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15,137]) ).
thf(159,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) @ axiom )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[158]) ).
thf(162,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ not @ or ) )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[159]) ).
thf(113,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ not @ or ) @ ( B @ ( A @ not @ or ) @ not @ or ) @ axiom )
!= ( D @ axiom ) )
| ~ $true
| ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[16,18]) ).
thf(114,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ not @ or ) @ ( B @ ( A @ not @ or ) @ not @ or ) @ axiom )
!= ( D @ axiom ) )
| ( D @ theorem ) ),
inference(simp,[status(thm)],[113]) ).
thf(115,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ ( C @ ( A @ not @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[114:[bind(A,$thf( O )),bind(B,$thf( Q )),bind(C,$thf( P )),bind(D,$thf( Q @ ( P @ or ) @ ( O @ ( P @ or ) @ not @ or ) @ ( Q @ ( O @ not @ or ) @ not @ or ) ))]]) ).
thf(123,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ ( C @ ( A @ not @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[115]) ).
thf(6803,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( q @ not @ not @ ( p @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,6709]) ).
thf(6804,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( q @ not @ not @ ( p @ or ) @ theorem ) ),
inference(simp,[status(thm)],[6803]) ).
thf(6821,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( q @ not @ not @ ( p @ or ) ) ),
inference(simp,[status(thm)],[6804]) ).
thf(2506,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( C @ theorem ) )
| ( ( B @ ( C @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,924]) ).
thf(2507,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( C @ theorem ) )
| ( ( B @ ( C @ or ) )
!= p ) ),
inference(simp,[status(thm)],[2506]) ).
thf(2508,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ not @ or ) @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[2507:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ ( E @ not @ or ) ))]]) ).
thf(2582,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ not @ or ) @ or ) )
!= p ),
inference(simp,[status(thm)],[2508]) ).
thf(191,plain,
! [B: $i,A: $i] :
( ( A != p )
| ( B != r )
| ( A
!= ( r @ ( q @ not @ or ) ) ) ),
inference(simp,[status(thm)],[165]) ).
thf(194,plain,
( ( r @ ( q @ not @ or ) )
!= p ),
inference(simp,[status(thm)],[191]) ).
thf(133,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[122,11]) ).
thf(134,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[133]) ).
thf(145,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ not @ or ) )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[134]) ).
thf(5746,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[2347,86]) ).
thf(5747,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[5746]) ).
thf(5748,plain,
~ ( p @ ( q @ or ) @ not @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[5747:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( p @ ( q @ or ) @ not ))]]) ).
thf(7926,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( B @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4323,500]) ).
thf(7927,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( B @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p ) ),
inference(simp,[status(thm)],[7926]) ).
thf(7928,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ not @ ( A @ or ) @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[7927:[bind(A,$thf( E )),bind(B,$thf( G )),bind(C,$thf( G @ not @ ( E @ or ) )),bind(D,$thf( G ))]]) ).
thf(8163,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ not @ ( A @ or ) @ or ) )
!= p ),
inference(simp,[status(thm)],[7928]) ).
thf(4246,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2729,32]) ).
thf(4247,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4246]) ).
thf(4248,plain,
! [B: $i,A: $i] : ( A @ ( B @ not @ ( B @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4247:[bind(A,$thf( A )),bind(B,$thf( G )),bind(C,$thf( G @ not @ ( G @ or ) )),bind(D,$thf( A ))]]) ).
thf(4324,plain,
! [B: $i,A: $i] : ( A @ ( B @ not @ ( B @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[4248]) ).
thf(4515,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( C @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,4176]) ).
thf(4516,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( C @ ( p @ ( q @ or ) @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4515]) ).
thf(4517,plain,
! [A: $i] :
~ ( A @ ( p @ ( q @ or ) @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4516:[bind(A,$thf( F @ ( p @ ( q @ or ) @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( F ))]]) ).
thf(4561,plain,
! [A: $i] :
~ ( A @ ( p @ ( q @ or ) @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[4517]) ).
thf(4903,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[32,4677]) ).
thf(4904,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ ( A @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4903]) ).
thf(4905,plain,
~ ( r @ ( q @ not @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4904:[bind(A,$thf( r @ ( q @ not @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) ))]]) ).
thf(5751,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[126,86]) ).
thf(5752,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[5751]) ).
thf(5753,plain,
~ ( p @ ( q @ or ) @ not @ ( p @ ( r @ or ) @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[5752:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( p @ ( q @ or ) @ not @ ( p @ ( r @ or ) @ or ) ))]]) ).
thf(481,plain,
! [A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[229,468]) ).
thf(482,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( p @ theorem ) ),
inference(simp,[status(thm)],[481]) ).
thf(502,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) )
!= p ),
inference(simp,[status(thm)],[482]) ).
thf(11838,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[149,4871]) ).
thf(11839,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[11838]) ).
thf(11840,plain,
~ ( p @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[11839:[bind(A,$thf( q @ not @ ( r @ or ) )),bind(B,$thf( r )),bind(C,$thf( p ))]]) ).
thf(6152,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ not @ or ) @ ( B @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3468,500]) ).
thf(6153,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ not @ or ) @ ( B @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p ) ),
inference(simp,[status(thm)],[6152]) ).
thf(6154,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ not @ or ) @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[6153:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( F @ ( G @ not @ or ) )),bind(D,$thf( G ))]]) ).
thf(6333,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ not @ or ) @ or ) )
!= p ),
inference(simp,[status(thm)],[6154]) ).
thf(2653,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( q @ ( p @ or ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,2382]) ).
thf(2654,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( q @ ( p @ or ) @ not @ theorem ) ),
inference(simp,[status(thm)],[2653]) ).
thf(2711,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( q @ ( p @ or ) @ not ) ),
inference(simp,[status(thm)],[2654]) ).
thf(2558,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( C @ theorem ) )
| ( ( C @ ( B @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,501]) ).
thf(2559,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( C @ theorem ) )
| ( ( C @ ( B @ or ) )
!= p ) ),
inference(simp,[status(thm)],[2558]) ).
thf(2560,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ not @ or ) @ ( A @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[2559:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ ( E @ not @ or ) ))]]) ).
thf(2579,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ not @ or ) @ ( A @ or ) )
!= p ),
inference(simp,[status(thm)],[2560]) ).
thf(2648,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( ( B @ ( C @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,924]) ).
thf(2649,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( ( B @ ( C @ or ) )
!= p ) ),
inference(simp,[status(thm)],[2648]) ).
thf(2650,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ not @ ( B @ or ) @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[2649:[bind(A,$thf( F )),bind(B,$thf( B )),bind(C,$thf( F @ not @ ( F @ or ) ))]]) ).
thf(2728,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ not @ ( B @ or ) @ or ) )
!= p ),
inference(simp,[status(thm)],[2650]) ).
thf(6888,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( q @ not @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,6778]) ).
thf(6889,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( q @ not @ not @ theorem ) ),
inference(simp,[status(thm)],[6888]) ).
thf(6917,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( q @ not @ not ) ),
inference(simp,[status(thm)],[6889]) ).
thf(589,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[228,501]) ).
thf(590,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p ) ),
inference(simp,[status(thm)],[589]) ).
thf(591,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[590:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ or ) @ or ) ))]]) ).
thf(612,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) )
!= p ),
inference(simp,[status(thm)],[591]) ).
thf(491,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[124,468]) ).
thf(492,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( p @ theorem ) ),
inference(simp,[status(thm)],[491]) ).
thf(497,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ not @ or ) )
!= p ),
inference(simp,[status(thm)],[492]) ).
thf(844,plain,
! [A: $i] :
( ( A != p )
| ( ( A @ ( A @ or ) @ not )
!= r ) ),
inference(simp,[status(thm)],[480]) ).
thf(845,plain,
( ( p @ ( p @ or ) @ not )
!= r ),
inference(simp,[status(thm)],[844]) ).
thf(2437,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ ( p @ or ) @ not @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,2382]) ).
thf(2438,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ ( p @ or ) @ not @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2437]) ).
thf(2479,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( q @ ( p @ or ) @ not ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2438]) ).
thf(5800,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( q @ not @ ( r @ or ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,5621]) ).
thf(5801,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( q @ not @ ( r @ or ) @ not @ theorem ) ),
inference(simp,[status(thm)],[5800]) ).
thf(5860,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( q @ not @ ( r @ or ) @ not ) ),
inference(simp,[status(thm)],[5801]) ).
thf(11039,plain,
( ( q @ ( p @ or ) )
!= p ),
inference(simp,[status(thm)],[11038]) ).
thf(7565,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ or ) @ ( C @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,7544]) ).
thf(7566,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ or ) @ ( C @ or ) @ not @ ( p @ or ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[7565]) ).
thf(7567,plain,
! [A: $i] :
~ ( p @ ( q @ or ) @ ( A @ or ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[7566:[bind(A,$thf( p )),bind(B,$thf( p @ ( q @ or ) @ ( E @ or ) @ not )),bind(C,$thf( E ))]]) ).
thf(7638,plain,
! [A: $i] :
~ ( p @ ( q @ or ) @ ( A @ or ) @ not @ theorem ),
inference(simp,[status(thm)],[7567]) ).
thf(5145,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,5044]) ).
thf(5146,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[5145]) ).
thf(5162,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( p @ ( r @ ( q @ not @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[5146]) ).
thf(5348,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3453,500]) ).
thf(5349,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( ( D @ ( C @ or ) )
!= p ) ),
inference(simp,[status(thm)],[5348]) ).
thf(5350,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ or ) @ ( B @ not @ or ) )
!= p ),
inference(pattern_uni,[status(thm)],[5349:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( G @ not )),bind(D,$thf( F @ ( G @ or ) ))]]) ).
thf(5517,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ or ) @ ( B @ not @ or ) )
!= p ),
inference(simp,[status(thm)],[5350]) ).
thf(72,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( D @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( D @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom )
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[22,54]) ).
thf(73,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( D @ not @ or ) @ theorem ) )
| ~ ( D @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom )
| ~ ( B @ ( C @ not @ or ) @ theorem )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[72]) ).
thf(74,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( B @ not @ or ) @ theorem )
| ~ ( B @ ( A @ not @ or ) @ axiom ) ),
inference(pattern_uni,[status(thm)],[73:[bind(A,$thf( A )),bind(B,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(82,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( B @ not @ or ) @ theorem )
| ~ ( B @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[74]) ).
thf(2160,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[1043,54]) ).
thf(2161,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( C @ not @ or ) @ theorem ) )
| ~ ( C @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[2160]) ).
thf(2162,plain,
~ ( p @ ( r @ or ) @ ( p @ ( r @ or ) @ or ) @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[2161:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( p @ ( r @ or ) )),bind(C,$thf( p @ ( r @ or ) @ ( p @ ( r @ or ) @ or ) ))]]) ).
thf(6772,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( q @ not @ not @ ( p @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,6709]) ).
thf(6773,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( q @ not @ not @ ( p @ or ) @ theorem ) ),
inference(simp,[status(thm)],[6772]) ).
thf(6822,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( q @ not @ not @ ( p @ or ) ) ),
inference(simp,[status(thm)],[6773]) ).
thf(142,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[122,68]) ).
thf(143,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[142]) ).
thf(146,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ not @ or ) )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[143]) ).
thf(11982,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( D @ or ) @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[149,4178]) ).
thf(11983,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( D @ or ) @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[11982]) ).
thf(11984,plain,
! [A: $i] :
~ ( p @ ( p @ ( A @ or ) @ ( q @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[11983:[bind(A,$thf( p @ ( G @ or ) @ ( q @ or ) )),bind(B,$thf( r )),bind(C,$thf( p )),bind(D,$thf( G ))]]) ).
thf(12081,plain,
! [A: $i] :
~ ( p @ ( p @ ( A @ or ) @ ( q @ or ) @ not @ or ) @ axiom ),
inference(simp,[status(thm)],[11984]) ).
thf(2048,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( B @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[124,457]) ).
thf(2049,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( B @ not @ or ) @ theorem ) )
| ~ ( B @ ( p @ ( q @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[2048]) ).
thf(2050,plain,
~ ( p @ ( r @ or ) @ ( p @ ( r @ or ) @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[2049:[bind(A,$thf( p @ ( r @ or ) )),bind(B,$thf( p @ ( r @ or ) @ ( p @ ( r @ or ) @ or ) ))]]) ).
thf(5116,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,5044]) ).
thf(5117,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( p @ ( r @ ( q @ not @ or ) @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[5116]) ).
thf(5172,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( p @ ( r @ ( q @ not @ or ) @ not @ or ) ) ),
inference(simp,[status(thm)],[5117]) ).
thf(11198,plain,
! [A: $i] :
( ( ( A @ not )
!= p )
| ( A
!= ( r @ ( q @ not @ or ) @ not ) ) ),
inference(simp,[status(thm)],[5172]) ).
thf(11199,plain,
( ( r @ ( q @ not @ or ) @ not @ not )
!= p ),
inference(simp,[status(thm)],[11198]) ).
thf(4979,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[64,4871]) ).
thf(4980,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4979]) ).
thf(4981,plain,
~ ( p @ ( q @ not @ ( r @ or ) @ not @ or ) @ ( r @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4980:[bind(A,$thf( q @ not @ ( r @ or ) @ not )),bind(B,$thf( r )),bind(C,$thf( p ))]]) ).
thf(77,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ axiom )
!= ( B @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( B @ not @ or ) @ theorem )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[12,54]) ).
thf(78,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) @ axiom )
!= ( B @ ( r @ ( q @ not @ or ) @ not @ or ) @ axiom ) )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( B @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[77]) ).
thf(79,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ not @ or ) )
!= ( B @ ( r @ ( q @ not @ or ) @ not @ or ) ) )
| ~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( B @ not @ or ) @ theorem ) ),
inference(simp,[status(thm)],[78]) ).
thf(2511,plain,
! [A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( q @ ( p @ or ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2314,2382]) ).
thf(2512,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) @ theorem )
!= ( q @ ( p @ or ) @ not @ theorem ) ),
inference(simp,[status(thm)],[2511]) ).
thf(2572,plain,
! [A: $i] :
( ( A @ ( A @ not @ or ) )
!= ( q @ ( p @ or ) @ not ) ),
inference(simp,[status(thm)],[2512]) ).
thf(5534,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ or ) @ theorem )
!= ( r @ ( q @ not @ or ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2586,5279]) ).
thf(5535,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) @ theorem )
!= ( r @ ( q @ not @ or ) @ not @ theorem ) ),
inference(simp,[status(thm)],[5534]) ).
thf(5586,plain,
! [A: $i] :
( ( A @ not @ ( A @ or ) )
!= ( r @ ( q @ not @ or ) @ not ) ),
inference(simp,[status(thm)],[5535]) ).
thf(696,plain,
! [B: $i,A: $i] :
( ( ( B @ not )
!= p )
| ( ( B @ ( A @ or ) )
!= r ) ),
inference(simp,[status(thm)],[476]) ).
thf(11784,plain,
( ( q @ not @ ( r @ or ) )
!= p ),
inference(simp,[status(thm)],[11783]) ).
thf(9985,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( D @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( D @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[125,86]) ).
thf(9986,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ ( B @ or ) @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( D @ not @ or ) @ theorem ) )
| ~ ( D @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[9985]) ).
thf(9987,plain,
~ ( p @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[9986:[bind(A,$thf( p @ ( q @ or ) @ not )),bind(B,$thf( r )),bind(C,$thf( p )),bind(D,$thf( p @ ( p @ ( q @ or ) @ not @ or ) @ ( r @ or ) ))]]) ).
thf(863,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[424,32]) ).
thf(864,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[863]) ).
thf(865,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ not @ ( C @ ( B @ or ) @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[864:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( J )),bind(D,$thf( J @ not @ ( J @ ( H @ or ) @ or ) )),bind(E,$thf( A ))]]) ).
thf(897,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ not @ ( C @ ( B @ or ) @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[865]) ).
thf(5739,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( B @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( B @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[2314,86]) ).
thf(5740,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( B @ not @ or ) @ theorem ) )
| ~ ( B @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[5739]) ).
thf(5741,plain,
~ ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[5740:[bind(A,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) )),bind(B,$thf( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) ))]]) ).
thf(6145,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ not @ or ) @ ( B @ or ) @ theorem )
!= ( p @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3468,468]) ).
thf(6146,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ not @ or ) @ ( B @ or ) @ theorem )
!= ( p @ theorem ) ),
inference(simp,[status(thm)],[6145]) ).
thf(6316,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ not @ or ) @ ( B @ or ) )
!= p ),
inference(simp,[status(thm)],[6146]) ).
thf(6213,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ not @ or ) @ ( B @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[3468,32]) ).
thf(6214,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ not @ or ) @ ( B @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[6213]) ).
thf(6215,plain,
! [B: $i,A: $i] : ( B @ ( A @ ( B @ not @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[6214:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( F @ ( G @ not @ or ) )),bind(D,$thf( G ))]]) ).
thf(6348,plain,
! [B: $i,A: $i] : ( B @ ( A @ ( B @ not @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[6215]) ).
thf(11315,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( B @ ( B @ not @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[11027,32]) ).
thf(11316,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( B @ ( B @ not @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[11315]) ).
thf(11317,plain,
! [B: $i,A: $i] : ( A @ ( A @ not @ or ) @ ( B @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[11316:[bind(A,$thf( H )),bind(B,$thf( F )),bind(C,$thf( H @ not )),bind(D,$thf( F @ ( F @ not @ or ) ))]]) ).
thf(11489,plain,
! [B: $i,A: $i] : ( A @ ( A @ not @ or ) @ ( B @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[11317]) ).
thf(12005,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ ( p @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[149,2018]) ).
thf(12006,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ not @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( q @ ( p @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ not @ or ) @ axiom ) ),
inference(simp,[status(thm)],[12005]) ).
thf(12007,plain,
~ ( p @ ( q @ ( p @ or ) @ not @ or ) @ axiom ),
inference(pattern_uni,[status(thm)],[12006:[bind(A,$thf( q @ ( p @ or ) )),bind(B,$thf( r )),bind(C,$thf( p ))]]) ).
thf(4594,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( D @ or ) @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[64,4178]) ).
thf(4595,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( D @ or ) @ ( q @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4594]) ).
thf(4596,plain,
! [A: $i] :
~ ( p @ ( p @ ( A @ or ) @ ( q @ or ) @ not @ or ) @ ( r @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4595:[bind(A,$thf( p @ ( H @ or ) @ ( q @ or ) @ not )),bind(B,$thf( r )),bind(C,$thf( p )),bind(D,$thf( H ))]]) ).
thf(4642,plain,
! [A: $i] :
~ ( p @ ( p @ ( A @ or ) @ ( q @ or ) @ not @ or ) @ ( r @ or ) @ theorem ),
inference(simp,[status(thm)],[4596]) ).
thf(2877,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ $true
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[64,68]) ).
thf(2878,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( p @ ( r @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ theorem ) )
| ~ ( C @ ( A @ or ) @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2877]) ).
thf(2879,plain,
~ ( p @ ( r @ or ) @ ( q @ not @ ( r @ or ) @ not @ or ) @ ( p @ ( q @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2878:[bind(A,$thf( q @ not @ ( r @ or ) @ not )),bind(B,$thf( p @ ( q @ or ) @ not )),bind(C,$thf( p @ ( r @ or ) ))]]) ).
thf(25341,plain,
$false,
inference(e,[status(thm)],[6756,4560,8288,479,468,352,6744,2527,12089,2590,10,3217,56,500,8385,6909,8086,5621,11491,14,3131,11913,11010,125,4984,5279,20,606,228,57,4179,8571,46,1609,2237,924,3431,10746,376,3453,106,4871,2777,480,147,3189,11783,3406,2586,5738,8274,4643,428,12068,102,4100,2382,942,4323,5044,3134,165,11191,33,1238,2147,160,424,9849,192,693,21,137,229,65,97,2068,6402,3763,6709,3033,842,11488,2577,3963,2724,499,3386,2726,53,124,339,193,476,2085,4180,8159,96,933,7453,5576,7544,457,4902,2566,13,503,605,2729,5762,148,161,64,2028,17,444,149,32,34,176,3768,22,843,3086,4677,3458,641,1503,12,9984,54,498,11038,540,86,144,3330,604,7546,6920,81,2955,3468,1043,4176,98,3066,5511,1557,2314,609,10942,3192,2542,5863,7820,10147,5218,3953,80,431,5139,426,10749,162,123,6821,2582,194,145,640,5748,8163,4324,2888,18,5250,4561,4905,11027,16,370,5753,502,11840,5106,6333,2711,2579,11,2728,6917,3961,612,497,2865,845,231,2479,2347,5860,11039,55,7638,3324,5162,5517,82,478,2162,6822,146,12081,19,422,2050,4178,126,11199,4981,79,2572,10472,5586,2714,696,11784,9987,897,5741,6316,7915,2583,6348,15,10146,68,6778,501,11489,12007,5172,122,4642,2018,3052,3296,7548,2879]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL195-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.13 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.25/0.50 % Computer : n018.cluster.edu
% 0.25/0.50 % Model : x86_64 x86_64
% 0.25/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.25/0.50 % Memory : 8046.5625MB
% 0.25/0.50 % OS : Linux 6.8.0-71-generic
% 0.25/0.51 % CPULimit : 300
% 0.25/0.51 % WCLimit : 300
% 0.25/0.51 % DateTime : Fri Sep 25 22:02:21 UTC 2026
% 0.12/0.51 % CPUTime :
% 0.12/0.51 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.07/1.13 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.70/1.42 % [INFO] Parsing done (291ms).
% 1.70/1.44 % [INFO] Running in sequential loop mode.
% 2.79/2.09 % [INFO] eprover registered as external prover.
% 2.79/2.10 % [INFO] Scanning for conjecture ...
% 3.05/2.24 % [INFO] Found a conjecture (or negated_conjecture) and 8 axioms. Running axiom selection ...
% 3.05/2.29 % [INFO] Axiom selection finished. Selected 8 axioms (removed 0 axioms).
% 3.24/2.32 % [INFO] Problem is propositional (TPTP CNF).
% 3.24/2.32 % [INFO] Type checking passed.
% 3.24/2.33 % [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 ...
% 113.45/28.39 % External prover 'e' found a proof!
% 113.45/28.40 % [INFO] Killing All external provers ...
% 113.89/28.40 % Time passed: 27740ms (effective reasoning time: 26944ms)
% 113.89/28.40 % Axioms used in derivation (8): axiom_1_5, axiom_1_4, rule_1, axiom_1_3, rule_3, axiom_1_2, rule_2, axiom_1_6
% 113.89/28.40 % No. of inferences in proof: 796
% 113.89/28.40 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 27740 ms resp. 26944 ms w/o parsing
% 107.23/28.69 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 107.23/28.69 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------