%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LCL335-3 : TPTP v9.3.1. Released v2.3.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 : n002.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:32 AM UTC 2026
% Result : Unsatisfiable 260.27s 74.10s
% Output : Refutation 259.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 11
% Syntax : Number of formulae : 560 ( 271 unt; 0 typ; 0 def)
% Number of atoms : 1428 ( 429 equ; 0 cnn)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 7194 ( 607 ~; 424 |; 0 &;6163 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 7 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 13 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 1498 ( 0 ^;1498 !; 0 ?;1498 :)
% Comments :
%------------------------------------------------------------------------------
thf(theorem_decl,type,
theorem: $i > $o ).
thf(implies_decl,type,
implies: $i > $i > $i ).
thf(and_decl,type,
and: $i > $i > $i ).
thf(p_decl,type,
p: $i ).
thf(q_decl,type,
q: $i ).
thf(r_decl,type,
r: $i ).
thf(equivalent_decl,type,
equivalent: $i > $i > $i ).
thf(axiom_decl,type,
axiom: $i > $o ).
thf(or_decl,type,
or: $i > $i > $i ).
thf(not_decl,type,
not: $i > $i ).
thf(7,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) )
= ( B @ ( A @ not @ or ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',implies_definition) ).
thf(19,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) )
= ( B @ ( A @ not @ or ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(20,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ not @ or ) )
= ( B @ ( A @ implies ) ) ),
inference(lifteq,[status(thm)],[19]) ).
thf(3,axiom,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ ( A @ implies ) @ axiom ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_3) ).
thf(15,plain,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ ( A @ implies ) @ axiom ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(31,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( D @ or ) ) )
| ( B @ ( A @ implies ) @ ( C @ implies ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[20,15]) ).
thf(32,plain,
! [B: $i,A: $i] : ( A @ ( B @ implies ) @ ( A @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[31:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( E @ not ))]]) ).
thf(33,plain,
! [B: $i,A: $i] : ( A @ ( B @ implies ) @ ( A @ implies ) @ axiom ),
inference(simp,[status(thm)],[32]) ).
thf(8,axiom,
! [A: $i] :
( ~ ( A @ axiom )
| ( A @ theorem ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_1) ).
thf(21,plain,
! [A: $i] :
( ~ ( A @ axiom )
| ( A @ theorem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(22,plain,
! [A: $i] :
( ~ ( A @ axiom )
| ( A @ theorem ) ),
inference(cnf,[status(esa)],[21]) ).
thf(41,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ implies ) @ ( A @ implies ) @ axiom )
!= ( C @ axiom ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[33,22]) ).
thf(42,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ implies ) @ ( A @ implies ) @ axiom )
!= ( C @ axiom ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[41]) ).
thf(43,plain,
! [B: $i,A: $i] : ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[42:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( G @ ( F @ implies ) @ ( G @ implies ) ))]]) ).
thf(48,plain,
! [B: $i,A: $i] : ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem ),
inference(simp,[status(thm)],[43]) ).
thf(9,axiom,
! [B: $i,A: $i] :
( ~ ( B @ theorem )
| ~ ( A @ ( B @ implies ) @ theorem )
| ( A @ theorem ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_2) ).
thf(23,plain,
! [B: $i,A: $i] :
( ~ ( B @ theorem )
| ~ ( A @ ( B @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(24,plain,
! [B: $i,A: $i] :
( ~ ( B @ theorem )
| ~ ( A @ ( B @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(cnf,[status(esa)],[23]) ).
thf(80,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( C @ ( D @ implies ) @ theorem ) )
| ~ ( D @ theorem )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[48,24]) ).
thf(81,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( C @ ( D @ implies ) @ theorem ) )
| ~ ( D @ theorem )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[80]) ).
thf(82,plain,
! [B: $i,A: $i] :
( ~ ( B @ theorem )
| ( B @ ( A @ implies ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[81:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ implies ) )),bind(D,$thf( F ))]]) ).
thf(90,plain,
! [B: $i,A: $i] :
( ~ ( B @ theorem )
| ( B @ ( A @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[82]) ).
thf(951,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[48,90]) ).
thf(952,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[951]) ).
thf(953,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[952:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ implies ) @ ( H @ implies ) ))]]) ).
thf(991,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[953]) ).
thf(1152,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[991,90]) ).
thf(1153,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[1152]) ).
thf(1154,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1153:[bind(A,$thf( F )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( J @ implies ) @ ( K @ implies ) @ ( F @ implies ) ))]]) ).
thf(1185,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[1154]) ).
thf(6,axiom,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ implies ) @ ( B @ ( A @ implies ) @ implies ) @ axiom ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_6) ).
thf(18,plain,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ implies ) @ ( B @ ( A @ implies ) @ implies ) @ axiom ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(219,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ implies ) @ ( B @ ( A @ implies ) @ implies ) @ axiom )
!= ( D @ axiom ) )
| ~ $true
| ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[18,22]) ).
thf(220,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ or ) @ ( A @ ( C @ or ) @ implies ) @ ( B @ ( A @ implies ) @ implies ) @ axiom )
!= ( D @ axiom ) )
| ( D @ theorem ) ),
inference(simp,[status(thm)],[219]) ).
thf(221,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ implies ) @ ( C @ ( A @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[220:[bind(A,$thf( L )),bind(B,$thf( N )),bind(C,$thf( M )),bind(D,$thf( N @ ( M @ or ) @ ( L @ ( M @ or ) @ implies ) @ ( N @ ( L @ implies ) @ implies ) ))]]) ).
thf(224,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ implies ) @ ( C @ ( A @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[221]) ).
thf(2,axiom,
! [A: $i] : ( A @ ( A @ ( A @ or ) @ implies ) @ axiom ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_2) ).
thf(14,plain,
! [A: $i] : ( A @ ( A @ ( A @ or ) @ implies ) @ axiom ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(38,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ axiom )
!= ( B @ axiom ) )
| ~ $true
| ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[14,22]) ).
thf(39,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ axiom )
!= ( B @ axiom ) )
| ( B @ theorem ) ),
inference(simp,[status(thm)],[38]) ).
thf(40,plain,
! [A: $i] : ( A @ ( A @ ( A @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[39:[bind(A,$thf( D )),bind(B,$thf( D @ ( D @ ( D @ or ) @ implies ) ))]]) ).
thf(47,plain,
! [A: $i] : ( A @ ( A @ ( A @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[40]) ).
thf(57,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ~ ( B @ ( C @ implies ) @ theorem )
| ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[47,24]) ).
thf(58,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( C @ theorem ) )
| ~ ( B @ ( C @ implies ) @ theorem )
| ( B @ theorem ) ),
inference(simp,[status(thm)],[57]) ).
thf(59,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ ( B @ ( B @ or ) @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[58:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ ( E @ ( E @ or ) @ implies ) ))]]) ).
thf(66,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ ( B @ ( B @ or ) @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[59]) ).
thf(563,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ implies ) @ ( C @ ( A @ implies ) @ implies ) @ theorem )
!= ( D @ ( E @ ( E @ ( E @ or ) @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[224,66]) ).
thf(564,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ implies ) @ ( C @ ( A @ implies ) @ implies ) @ theorem )
!= ( D @ ( E @ ( E @ ( E @ or ) @ implies ) @ implies ) @ theorem ) )
| ( D @ theorem ) ),
inference(simp,[status(thm)],[563]) ).
thf(565,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ ( A @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[564:[bind(A,$thf( O @ ( O @ or ) )),bind(B,$thf( N )),bind(C,$thf( O )),bind(D,$thf( O @ ( N @ or ) @ ( O @ ( O @ or ) @ ( N @ or ) @ implies ) )),bind(E,$thf( O ))]]) ).
thf(594,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ ( A @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[565]) ).
thf(831,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( D @ or ) @ ( C @ or ) ) )
| ( D @ ( C @ or ) @ ( B @ ( A @ implies ) @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,594]) ).
thf(832,plain,
! [B: $i,A: $i] : ( B @ ( A @ not @ or ) @ ( B @ ( B @ or ) @ ( A @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[831:[bind(A,$thf( E )),bind(B,$thf( G @ ( G @ or ) )),bind(C,$thf( E @ not )),bind(D,$thf( G ))]]) ).
thf(850,plain,
! [B: $i,A: $i] : ( B @ ( A @ not @ or ) @ ( B @ ( B @ or ) @ ( A @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[832]) ).
thf(858,plain,
! [B: $i,A: $i] : ( B @ ( A @ implies ) @ ( B @ ( B @ or ) @ ( A @ implies ) @ implies ) @ theorem ),
inference(rewrite,[status(thm)],[850,20]) ).
thf(44,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ implies ) @ axiom )
!= ( C @ axiom ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[15,22]) ).
thf(45,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( A @ implies ) @ axiom )
!= ( C @ axiom ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[44]) ).
thf(46,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( B @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[45:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( G @ ( F @ or ) @ ( G @ implies ) ))]]) ).
thf(49,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( B @ implies ) @ theorem ),
inference(simp,[status(thm)],[46]) ).
thf(100,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ~ ( C @ ( D @ implies ) @ theorem )
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[49,24]) ).
thf(101,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ ( C @ ( D @ implies ) @ theorem )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[100]) ).
thf(102,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ or ) @ ( C @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[101:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ or ) @ ( H @ implies ) ))]]) ).
thf(108,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ or ) @ ( C @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[102]) ).
thf(2357,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ ( B @ or ) @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ ( E @ ( D @ or ) @ ( E @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[858,108]) ).
thf(2358,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ ( B @ or ) @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ ( E @ ( D @ or ) @ ( E @ implies ) @ implies ) @ theorem ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[2357]) ).
thf(2359,plain,
! [A: $i] : ( A @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2358:[bind(A,$thf( G )),bind(B,$thf( G )),bind(C,$thf( G @ ( G @ implies ) )),bind(D,$thf( G )),bind(E,$thf( G ))]]) ).
thf(2429,plain,
! [A: $i] : ( A @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2359]) ).
thf(97,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( C @ ( D @ implies ) @ theorem ) )
| ~ ( D @ theorem )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[49,24]) ).
thf(98,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( C @ ( D @ implies ) @ theorem ) )
| ~ ( D @ theorem )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[97]) ).
thf(99,plain,
! [B: $i,A: $i] :
( ~ ( B @ theorem )
| ( B @ ( A @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[98:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ or ) )),bind(D,$thf( F ))]]) ).
thf(107,plain,
! [B: $i,A: $i] :
( ~ ( B @ theorem )
| ( B @ ( A @ or ) @ theorem ) ),
inference(simp,[status(thm)],[99]) ).
thf(2472,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2429,107]) ).
thf(2473,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2472]) ).
thf(2474,plain,
! [B: $i,A: $i] : ( B @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2473:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ ( E @ implies ) ))]]) ).
thf(2486,plain,
! [B: $i,A: $i] : ( B @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2474]) ).
thf(2535,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2486,90]) ).
thf(2536,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2535]) ).
thf(2537,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2536:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ implies ) @ ( E @ or ) ))]]) ).
thf(2551,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2537]) ).
thf(2802,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2551,107]) ).
thf(2803,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2802]) ).
thf(2804,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ or ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2803:[bind(A,$thf( F )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( K @ implies ) @ ( H @ or ) @ ( F @ implies ) ))]]) ).
thf(2822,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ or ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2804]) ).
thf(4,axiom,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ implies ) @ axiom ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_4) ).
thf(16,plain,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ implies ) @ axiom ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(72,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ implies ) @ axiom )
!= ( C @ axiom ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[16,22]) ).
thf(73,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ implies ) @ axiom )
!= ( C @ axiom ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[72]) ).
thf(74,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[73:[bind(A,$thf( I )),bind(B,$thf( H )),bind(C,$thf( I @ ( H @ or ) @ ( H @ ( I @ or ) @ implies ) ))]]) ).
thf(77,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[74]) ).
thf(160,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( B @ ( A @ implies ) @ ( C @ ( D @ or ) @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,77]) ).
thf(161,plain,
! [B: $i,A: $i] : ( A @ ( B @ implies ) @ ( B @ not @ ( A @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[160:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(176,plain,
! [B: $i,A: $i] : ( A @ ( B @ implies ) @ ( B @ not @ ( A @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[161]) ).
thf(232,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ not @ ( C @ or ) ) )
| ( C @ ( D @ implies ) @ ( B @ ( A @ implies ) @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,176]) ).
thf(233,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ implies ) @ ( B @ not @ ( A @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[232:[bind(A,$thf( E )),bind(B,$thf( F @ not )),bind(C,$thf( E @ not )),bind(D,$thf( F ))]]) ).
thf(247,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ implies ) @ ( B @ not @ ( A @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[233]) ).
thf(558,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( B @ implies ) @ ( B @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ ( D @ ( D @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[247,66]) ).
thf(559,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( B @ implies ) @ ( B @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ ( D @ ( D @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[558]) ).
thf(560,plain,
! [A: $i] : ( A @ not @ ( A @ not @ or ) @ not @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[559:[bind(A,$thf( N @ not @ ( N @ not @ or ) )),bind(B,$thf( N )),bind(C,$thf( N @ not @ ( N @ not @ or ) @ not @ ( N @ implies ) )),bind(D,$thf( N @ not ))]]) ).
thf(590,plain,
! [A: $i] : ( A @ not @ ( A @ not @ or ) @ not @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[560]) ).
thf(629,plain,
! [A: $i] : ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem ),
inference(rewrite,[status(thm)],[590,20]) ).
thf(2475,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2429,90]) ).
thf(2476,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2475]) ).
thf(2477,plain,
! [B: $i,A: $i] : ( B @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2476:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ ( E @ implies ) ))]]) ).
thf(2487,plain,
! [B: $i,A: $i] : ( B @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2477]) ).
thf(2600,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ implies ) @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2487,90]) ).
thf(2601,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ implies ) @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2600]) ).
thf(2602,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2601:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ implies ) @ ( E @ implies ) ))]]) ).
thf(2612,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2602]) ).
thf(50,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( C @ or ) ) )
| ( C @ ( B @ ( A @ implies ) @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,47]) ).
thf(51,plain,
! [A: $i] : ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[50:[bind(A,$thf( E )),bind(B,$thf( E @ not )),bind(C,$thf( E @ not ))]]) ).
thf(64,plain,
! [A: $i] : ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[51]) ).
thf(35,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( A @ ( B @ implies ) @ theorem )
!= ( B @ theorem ) )
| ~ ( B @ theorem )
| ( A @ theorem ) ),
inference(eqfactor_ordered,[status(thm)],[24]) ).
thf(37,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) )
!= B )
| ~ ( B @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[35]) ).
thf(132,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( ( B @ ( C @ implies ) )
!= C )
| ~ $true
| ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[64,37]) ).
thf(133,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( ( B @ ( C @ implies ) )
!= C )
| ( B @ theorem ) ),
inference(simp,[status(thm)],[132]) ).
thf(134,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ implies ) )
!= ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) ) )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[133:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ not @ ( I @ not @ ( I @ implies ) @ implies ) ))]]) ).
thf(138,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ implies ) )
!= ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) ) )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[134]) ).
thf(2341,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ implies ) @ ( C @ ( A @ implies ) @ implies ) @ theorem )
!= ( D @ ( F @ ( E @ or ) @ ( F @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[224,108]) ).
thf(2342,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ implies ) @ ( C @ ( A @ implies ) @ implies ) @ theorem )
!= ( D @ ( F @ ( E @ or ) @ ( F @ implies ) @ implies ) @ theorem ) )
| ( D @ theorem ) ),
inference(simp,[status(thm)],[2341]) ).
thf(2343,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2342:[bind(A,$thf( P )),bind(B,$thf( M )),bind(C,$thf( P @ ( O @ or ) )),bind(D,$thf( P @ ( O @ or ) @ ( M @ or ) @ ( P @ ( M @ or ) @ implies ) )),bind(E,$thf( O )),bind(F,$thf( P ))]]) ).
thf(2427,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[2343]) ).
thf(1,negated_conjecture,
~ ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) @ theorem ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
thf(12,plain,
~ ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) @ theorem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(13,plain,
~ ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) @ theorem ),
inference(polarity_switch,[status(thm)],[12]) ).
thf(10,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ and ) )
= ( B @ not @ ( A @ not @ or ) @ not ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_defn) ).
thf(25,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ and ) )
= ( B @ not @ ( A @ not @ or ) @ not ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(26,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ and ) )
= ( B @ not @ ( A @ not @ or ) @ not ) ),
inference(lifteq,[status(thm)],[25]) ).
thf(181,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ and ) )
= ( B @ not @ ( A @ implies ) @ not ) ),
inference(rewrite,[status(thm)],[26,20]) ).
thf(184,plain,
~ ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ implies ) @ theorem ),
inference(rewrite,[status(thm)],[13,181]) ).
thf(11,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ equivalent ) )
= ( A @ ( B @ implies ) @ ( B @ ( A @ implies ) @ and ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equivalent_defn) ).
thf(27,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ equivalent ) )
= ( A @ ( B @ implies ) @ ( B @ ( A @ implies ) @ and ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(28,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ equivalent ) )
= ( A @ ( B @ implies ) @ ( B @ ( A @ implies ) @ and ) ) ),
inference(lifteq,[status(thm)],[27]) ).
thf(287,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ equivalent ) )
= ( A @ ( B @ implies ) @ not @ ( B @ ( A @ implies ) @ implies ) @ not ) ),
inference(rewrite,[status(thm)],[28,181]) ).
thf(292,plain,
~ ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ implies ) @ theorem ),
inference(rewrite,[status(thm)],[184,287]) ).
thf(922,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ implies ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[90,292]) ).
thf(923,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ implies ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[922]) ).
thf(924,plain,
~ ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[923:[bind(A,$thf( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not )),bind(B,$thf( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ))]]) ).
thf(2503,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2486,924]) ).
thf(2504,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2503]) ).
thf(2544,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ implies ) @ ( A @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(simp,[status(thm)],[2504]) ).
thf(162,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( D @ or ) ) )
| ( D @ ( C @ or ) @ ( B @ ( A @ implies ) @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,77]) ).
thf(163,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[162:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( E @ not ))]]) ).
thf(177,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[163]) ).
thf(578,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem )
!= ( C @ ( D @ ( D @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[177,66]) ).
thf(579,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem )
!= ( C @ ( D @ ( D @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[578]) ).
thf(580,plain,
! [A: $i] : ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[579:[bind(A,$thf( K )),bind(B,$thf( K @ ( K @ or ) )),bind(C,$thf( K @ ( K @ or ) @ not @ ( K @ or ) )),bind(D,$thf( K ))]]) ).
thf(593,plain,
! [A: $i] : ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[580]) ).
thf(901,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[593,90]) ).
thf(902,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[901]) ).
thf(903,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[902:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( H @ ( H @ or ) @ not @ ( H @ or ) ))]]) ).
thf(977,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[903]) ).
thf(1730,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[49,107]) ).
thf(1731,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1730]) ).
thf(1732,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1731:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ or ) @ ( H @ implies ) ))]]) ).
thf(1802,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1732]) ).
thf(1867,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1802,107]) ).
thf(1868,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1867]) ).
thf(1869,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1868:[bind(A,$thf( F )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( J @ or ) @ ( K @ implies ) @ ( F @ or ) ))]]) ).
thf(1882,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1869]) ).
thf(2933,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2612,107]) ).
thf(2934,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2933]) ).
thf(2935,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2934:[bind(A,$thf( F )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( K @ implies ) @ ( H @ implies ) @ ( F @ implies ) ))]]) ).
thf(2953,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2935]) ).
thf(2376,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem )
!= ( C @ ( E @ ( D @ or ) @ ( E @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[177,108]) ).
thf(2377,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem )
!= ( C @ ( E @ ( D @ or ) @ ( E @ implies ) @ implies ) @ theorem ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[2376]) ).
thf(2378,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2377:[bind(A,$thf( L @ ( J @ or ) )),bind(B,$thf( L )),bind(C,$thf( L @ not @ ( L @ ( J @ or ) @ or ) )),bind(D,$thf( J )),bind(E,$thf( L ))]]) ).
thf(2420,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[2378]) ).
thf(1005,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[90,924]) ).
thf(1006,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1005]) ).
thf(1007,plain,
~ ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1006:[bind(A,$thf( p )),bind(B,$thf( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ))]]) ).
thf(2640,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2420,1007]) ).
thf(2641,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[2640]) ).
thf(2671,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ or ) @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[2641]) ).
thf(939,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[49,90]) ).
thf(940,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[939]) ).
thf(941,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[940:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ or ) @ ( H @ implies ) ))]]) ).
thf(988,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[941]) ).
thf(1129,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[988,1007]) ).
thf(1130,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1129]) ).
thf(1142,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1130]) ).
thf(1032,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47,924]) ).
thf(1033,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[1032]) ).
thf(1044,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(simp,[status(thm)],[1033]) ).
thf(3377,plain,
! [A: $i] :
( ( A
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ( ( A @ ( A @ or ) )
!= p ) ),
inference(simp,[status(thm)],[1044]) ).
thf(3380,plain,
( ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ or ) )
!= p ),
inference(simp,[status(thm)],[3377]) ).
thf(3382,plain,
( ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ implies ) )
!= p ),
inference(rewrite,[status(thm)],[3380,20]) ).
thf(2440,plain,
! [A: $i] :
( ( ( A @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2429,924]) ).
thf(2441,plain,
! [A: $i] :
( ( A @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2440]) ).
thf(2478,plain,
! [A: $i] :
( ( A @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(simp,[status(thm)],[2441]) ).
thf(2685,plain,
! [A: $i] :
( ( A
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ( A != p ) ),
inference(simp,[status(thm)],[2478]) ).
thf(2686,plain,
( ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not )
!= p ),
inference(simp,[status(thm)],[2685]) ).
thf(5,axiom,
! [C: $i,B: $i,A: $i] : ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ implies ) @ axiom ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_5) ).
thf(17,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ implies ) @ axiom ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(149,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( E @ ( D @ or ) @ ( C @ or ) ) )
| ( E @ ( C @ or ) @ ( D @ or ) @ ( B @ ( A @ implies ) @ implies ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[20,17]) ).
thf(150,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( A @ not @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ implies ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[149:[bind(A,$thf( F )),bind(B,$thf( H @ ( G @ or ) )),bind(C,$thf( F @ not )),bind(D,$thf( G )),bind(E,$thf( H ))]]) ).
thf(157,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( A @ not @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ implies ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[150]) ).
thf(4839,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( A @ implies ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ implies ) @ implies ) @ axiom ),
inference(rewrite,[status(thm)],[157,20]) ).
thf(83,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ~ ( C @ ( D @ implies ) @ theorem )
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[48,24]) ).
thf(84,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ ( C @ ( D @ implies ) @ theorem )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[83]) ).
thf(85,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ implies ) @ ( C @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[84:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ implies ) @ ( H @ implies ) ))]]) ).
thf(91,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ implies ) @ ( C @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[85]) ).
thf(1233,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem )
!= ( C @ ( E @ ( D @ implies ) @ ( E @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[177,91]) ).
thf(1234,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem )
!= ( C @ ( E @ ( D @ implies ) @ ( E @ implies ) @ implies ) @ theorem ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[1233]) ).
thf(1235,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1234:[bind(A,$thf( L @ ( J @ implies ) )),bind(B,$thf( L )),bind(C,$thf( L @ not @ ( L @ ( J @ implies ) @ or ) )),bind(D,$thf( J )),bind(E,$thf( L ))]]) ).
thf(1261,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[1235]) ).
thf(1277,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1261,924]) ).
thf(1278,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[1277]) ).
thf(1296,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ implies ) @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(simp,[status(thm)],[1278]) ).
thf(5186,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ not @ ( D @ ( C @ implies ) @ or ) ) )
| ( ( B @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,1296]) ).
thf(5189,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ not ) )
| ( ( A @ not )
!= ( D @ ( C @ implies ) ) )
| ( B
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ( A != p ) ),
inference(simp,[status(thm)],[5186]) ).
thf(5192,plain,
! [B: $i,A: $i] :
( ( ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not )
!= ( B @ not ) )
| ( ( B @ ( A @ implies ) )
!= ( p @ not ) ) ),
inference(simp,[status(thm)],[5189]) ).
thf(1088,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47,1007]) ).
thf(1089,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1088]) ).
thf(1095,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1089]) ).
thf(2597,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ implies ) @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2487,107]) ).
thf(2598,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ implies ) @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2597]) ).
thf(2599,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2598:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ implies ) @ ( E @ implies ) ))]]) ).
thf(2611,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2599]) ).
thf(2868,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2611,90]) ).
thf(2869,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2868]) ).
thf(2870,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2869:[bind(A,$thf( F )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( K @ implies ) @ ( H @ implies ) @ ( F @ or ) ))]]) ).
thf(2886,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2870]) ).
thf(2532,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2486,107]) ).
thf(2533,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2532]) ).
thf(2534,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2533:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ implies ) @ ( E @ or ) ))]]) ).
thf(2550,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2534]) ).
thf(2737,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2550,90]) ).
thf(2738,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2737]) ).
thf(2739,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ or ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2738:[bind(A,$thf( F )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( K @ implies ) @ ( H @ or ) @ ( F @ or ) ))]]) ).
thf(2755,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ or ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2739]) ).
thf(1211,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ implies ) @ ( C @ ( A @ implies ) @ implies ) @ theorem )
!= ( D @ ( F @ ( E @ implies ) @ ( F @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[224,91]) ).
thf(1212,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ implies ) @ ( C @ ( A @ implies ) @ implies ) @ theorem )
!= ( D @ ( F @ ( E @ implies ) @ ( F @ implies ) @ implies ) @ theorem ) )
| ( D @ theorem ) ),
inference(simp,[status(thm)],[1211]) ).
thf(1213,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( A @ or ) @ ( C @ ( A @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1212:[bind(A,$thf( P )),bind(B,$thf( M )),bind(C,$thf( P @ ( O @ implies ) )),bind(D,$thf( P @ ( O @ implies ) @ ( M @ or ) @ ( P @ ( M @ or ) @ implies ) )),bind(E,$thf( O )),bind(F,$thf( P ))]]) ).
thf(1264,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( A @ or ) @ ( C @ ( A @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[1213]) ).
thf(1713,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)],[593,107]) ).
thf(1714,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1713]) ).
thf(1715,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1714:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( H @ ( H @ or ) @ not @ ( H @ or ) ))]]) ).
thf(1826,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1715]) ).
thf(1725,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[107,1007]) ).
thf(1726,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1725]) ).
thf(1797,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1726]) ).
thf(2018,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( B @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ~ ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,1797]) ).
thf(2019,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ~ ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[2018:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(2115,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ~ ( A @ theorem ) ),
inference(simp,[status(thm)],[2019]) ).
thf(2446,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ implies ) @ theorem )
!= ( B @ theorem ) )
| ( ( B @ ( C @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2429,2115]) ).
thf(2447,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ implies ) @ theorem )
!= ( B @ theorem ) )
| ( ( B @ ( C @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[2446]) ).
thf(2448,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(pattern_uni,[status(thm)],[2447:[bind(A,$thf( E )),bind(B,$thf( E @ ( E @ implies ) )),bind(C,$thf( C ))]]) ).
thf(2488,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[2448]) ).
thf(78,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,13]) ).
thf(79,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[78]) ).
thf(89,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(139,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) )
| ( B
!= ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) ) ) ),
inference(simp,[status(thm)],[89]) ).
thf(140,plain,
! [A: $i] :
( ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ ( A @ implies ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) ),
inference(simp,[status(thm)],[139]) ).
thf(141,plain,
! [A: $i] :
( ( ( r @ ( q @ equivalent ) )
!= ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) ) )
| ( A != p ) ),
inference(simp,[status(thm)],[140]) ).
thf(142,plain,
( ( r @ ( q @ equivalent ) )
!= ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) ) ),
inference(simp,[status(thm)],[141]) ).
thf(182,plain,
( ( r @ ( q @ equivalent ) )
!= ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(rewrite,[status(thm)],[142,181]) ).
thf(295,plain,
( ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not )
!= ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(rewrite,[status(thm)],[182,287]) ).
thf(296,plain,
( ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) )
!= ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) ) ),
inference(simp,[status(thm)],[295]) ).
thf(297,plain,
( ( ( q @ ( r @ implies ) @ not )
!= ( r @ ( q @ implies ) @ not ) )
| ( ( r @ ( q @ implies ) )
!= ( q @ ( p @ implies ) ) ) ),
inference(simp,[status(thm)],[296]) ).
thf(304,plain,
( ( ( q @ ( r @ implies ) )
!= ( r @ ( q @ implies ) ) )
| ( ( r @ ( q @ implies ) )
!= ( q @ ( p @ implies ) ) ) ),
inference(simp,[status(thm)],[297]) ).
thf(420,plain,
( ( ( r @ ( q @ implies ) )
!= ( r @ ( q @ implies ) ) )
| ( ( q @ ( r @ implies ) )
!= ( q @ ( p @ implies ) ) )
| ( ( r @ ( q @ implies ) )
!= ( q @ ( p @ implies ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[304]) ).
thf(421,plain,
( ( ( q @ ( r @ implies ) )
!= ( q @ ( p @ implies ) ) )
| ( ( r @ ( q @ implies ) )
!= ( q @ ( p @ implies ) ) ) ),
inference(simp,[status(thm)],[420]) ).
thf(166,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( C @ ( D @ implies ) @ theorem ) )
| ~ ( D @ theorem )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[77,24]) ).
thf(167,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( C @ ( D @ implies ) @ theorem ) )
| ~ ( D @ theorem )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[166]) ).
thf(168,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ or ) @ theorem )
| ( B @ ( A @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[167:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ or ) )),bind(D,$thf( G @ ( H @ or ) ))]]) ).
thf(178,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ or ) @ theorem )
| ( B @ ( A @ or ) @ theorem ) ),
inference(simp,[status(thm)],[168]) ).
thf(5857,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2486,178]) ).
thf(5858,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[5857]) ).
thf(5859,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[5858:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( F @ ( F @ implies ) )),bind(D,$thf( A ))]]) ).
thf(5990,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[5859]) ).
thf(6028,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ implies ) @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5990,1007]) ).
thf(6029,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ implies ) @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[6028]) ).
thf(6071,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ implies ) @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[6029]) ).
thf(1283,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1261,1007]) ).
thf(1284,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1283]) ).
thf(1302,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ implies ) @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1284]) ).
thf(169,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ~ ( C @ ( D @ implies ) @ theorem )
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[77,24]) ).
thf(170,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ ( C @ ( D @ implies ) @ theorem )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[169]) ).
thf(171,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[170:[bind(A,$thf( I )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( I @ or ) @ ( I @ ( J @ or ) @ implies ) ))]]) ).
thf(179,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[171]) ).
thf(575,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( C @ ( D @ ( D @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[48,66]) ).
thf(576,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( C @ ( D @ ( D @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[575]) ).
thf(577,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[576:[bind(A,$thf( I )),bind(B,$thf( L @ ( L @ ( L @ or ) @ implies ) )),bind(C,$thf( L @ ( L @ ( L @ or ) @ implies ) @ ( I @ implies ) )),bind(D,$thf( L ))]]) ).
thf(591,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[577]) ).
thf(1716,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[77,107]) ).
thf(1717,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1716]) ).
thf(1718,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1717:[bind(A,$thf( I )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( I @ or ) @ ( I @ ( J @ or ) @ implies ) ))]]) ).
thf(1828,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1718]) ).
thf(3149,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( D @ not @ ( B @ ( A @ implies ) @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ) ),
inference(paramod_ordered,[status(thm)],[20,2671]) ).
thf(3150,plain,
! [B: $i,A: $i] :
( ( A @ not @ ( A @ ( B @ implies ) @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(pattern_uni,[status(thm)],[3149:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(3152,plain,
! [B: $i,A: $i] :
( ( A @ not @ ( A @ ( B @ implies ) @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[3150]) ).
thf(1170,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[991,1007]) ).
thf(1171,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1170]) ).
thf(1183,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1171]) ).
thf(1697,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[107,924]) ).
thf(1698,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1697]) ).
thf(1796,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1698]) ).
thf(1220,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( C @ ( E @ ( D @ implies ) @ ( E @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[49,91]) ).
thf(1221,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( C @ ( E @ ( D @ implies ) @ ( E @ implies ) @ implies ) @ theorem ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[1220]) ).
thf(1222,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1221:[bind(A,$thf( J )),bind(B,$thf( O @ ( N @ implies ) @ ( O @ implies ) )),bind(C,$thf( O @ ( N @ implies ) @ ( O @ implies ) @ ( J @ or ) )),bind(D,$thf( N )),bind(E,$thf( O ))]]) ).
thf(1256,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1222]) ).
thf(1308,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1256,90]) ).
thf(1309,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[1308]) ).
thf(1310,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1309:[bind(A,$thf( F )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( J @ implies ) @ ( K @ implies ) @ ( F @ or ) ))]]) ).
thf(1351,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[1310]) ).
thf(305,plain,
( ( ( q @ ( r @ implies ) )
!= ( r @ ( q @ implies ) ) )
| ( r != q )
| ( q != p ) ),
inference(simp,[status(thm)],[297]) ).
thf(306,plain,
( ( r != q )
| ( r != q )
| ( r != q )
| ( q != p ) ),
inference(simp,[status(thm)],[305]) ).
thf(307,plain,
( ( r != q )
| ( q != p ) ),
inference(simp,[status(thm)],[306]) ).
thf(1024,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,924]) ).
thf(1025,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[1024]) ).
thf(1042,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(simp,[status(thm)],[1025]) ).
thf(129,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ~ ( B @ ( C @ implies ) @ theorem )
| ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[64,24]) ).
thf(130,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ theorem ) )
| ~ ( B @ ( C @ implies ) @ theorem )
| ( B @ theorem ) ),
inference(simp,[status(thm)],[129]) ).
thf(131,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[130:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ not @ ( I @ not @ ( I @ implies ) @ implies ) ))]]) ).
thf(137,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[131]) ).
thf(86,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( ( C @ ( D @ implies ) )
!= D )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[48,37]) ).
thf(87,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( ( C @ ( D @ implies ) )
!= D )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[86]) ).
thf(88,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ implies ) @ ( C @ implies ) @ implies ) )
!= ( C @ ( B @ implies ) @ ( C @ implies ) ) )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[87:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ implies ) @ ( H @ implies ) ))]]) ).
thf(92,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ implies ) @ ( C @ implies ) @ implies ) )
!= ( C @ ( B @ implies ) @ ( C @ implies ) ) )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[88]) ).
thf(5833,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2550,178]) ).
thf(5834,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[5833]) ).
thf(5835,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( C @ implies ) @ ( B @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[5834:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( I )),bind(D,$thf( I @ ( I @ implies ) @ ( F @ or ) )),bind(E,$thf( A ))]]) ).
thf(5983,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( C @ implies ) @ ( B @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[5835]) ).
thf(54,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( B @ ( C @ implies ) @ theorem ) )
| ~ ( C @ theorem )
| ~ $true
| ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[47,24]) ).
thf(55,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( B @ ( C @ implies ) @ theorem ) )
| ~ ( C @ theorem )
| ( B @ theorem ) ),
inference(simp,[status(thm)],[54]) ).
thf(56,plain,
! [A: $i] :
( ~ ( A @ ( A @ or ) @ theorem )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[55:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ ( E @ or ) ))]]) ).
thf(65,plain,
! [A: $i] :
( ~ ( A @ ( A @ or ) @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[56]) ).
thf(1699,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[591,107]) ).
thf(1700,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1699]) ).
thf(1701,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1700:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ ( H @ or ) @ implies ) @ ( E @ implies ) ))]]) ).
thf(1819,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1701]) ).
thf(874,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ ( B @ or ) @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ ( D @ ( D @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[858,66]) ).
thf(875,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ ( B @ or ) @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ ( D @ ( D @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[874]) ).
thf(876,plain,
! [A: $i] : ( A @ ( A @ ( A @ or ) @ ( A @ ( A @ or ) @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[875:[bind(A,$thf( J @ ( J @ or ) @ ( J @ ( J @ or ) @ or ) )),bind(B,$thf( J )),bind(C,$thf( J @ ( J @ ( J @ or ) @ ( J @ ( J @ or ) @ or ) @ implies ) )),bind(D,$thf( J @ ( J @ or ) ))]]) ).
thf(889,plain,
! [A: $i] : ( A @ ( A @ ( A @ or ) @ ( A @ ( A @ or ) @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[876]) ).
thf(1056,plain,
! [A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[593,1007]) ).
thf(1057,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1056]) ).
thf(1106,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1057]) ).
thf(572,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( C @ ( D @ ( D @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[49,66]) ).
thf(573,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( C @ ( D @ ( D @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[572]) ).
thf(574,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[573:[bind(A,$thf( I )),bind(B,$thf( L @ ( L @ ( L @ or ) @ implies ) )),bind(C,$thf( L @ ( L @ ( L @ or ) @ implies ) @ ( I @ or ) )),bind(D,$thf( L ))]]) ).
thf(595,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[574]) ).
thf(907,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[595,90]) ).
thf(908,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[907]) ).
thf(909,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[908:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ ( H @ or ) @ implies ) @ ( E @ or ) ))]]) ).
thf(980,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[909]) ).
thf(1074,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,1007]) ).
thf(1075,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1074]) ).
thf(1096,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1075]) ).
thf(103,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( ( C @ ( D @ implies ) )
!= D )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[49,37]) ).
thf(104,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( ( C @ ( D @ implies ) )
!= D )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[103]) ).
thf(105,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ or ) @ ( C @ implies ) @ implies ) )
!= ( C @ ( B @ or ) @ ( C @ implies ) ) )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[104:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ or ) @ ( H @ implies ) ))]]) ).
thf(109,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ or ) @ ( C @ implies ) @ implies ) )
!= ( C @ ( B @ or ) @ ( C @ implies ) ) )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[105]) ).
thf(5860,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1802,178]) ).
thf(5861,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[5860]) ).
thf(5862,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( B @ or ) @ ( C @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[5861:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( I )),bind(D,$thf( I @ ( H @ or ) @ ( I @ implies ) )),bind(E,$thf( A ))]]) ).
thf(5992,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( B @ or ) @ ( C @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[5862]) ).
thf(6013,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ implies ) @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5990,924]) ).
thf(6014,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ implies ) @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[6013]) ).
thf(6061,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( B @ implies ) @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(simp,[status(thm)],[6014]) ).
thf(6091,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( D @ ( D @ implies ) @ or ) ) )
| ( ( B @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,6061]) ).
thf(6094,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B != C )
| ( ( A @ not )
!= ( D @ ( D @ implies ) ) )
| ( B
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ( A != p ) ),
inference(simp,[status(thm)],[6091]) ).
thf(6097,plain,
! [A: $i] :
( ( A @ ( A @ implies ) )
!= ( p @ not ) ),
inference(simp,[status(thm)],[6094]) ).
thf(1018,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,924]) ).
thf(1019,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[1018]) ).
thf(1050,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(simp,[status(thm)],[1019]) ).
thf(2463,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( ( C @ ( B @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2429,1797]) ).
thf(2464,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( ( C @ ( B @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[2463]) ).
thf(2465,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ implies ) @ ( A @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(pattern_uni,[status(thm)],[2464:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ ( E @ implies ) ))]]) ).
thf(2482,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ implies ) @ ( A @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[2465]) ).
thf(1080,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,1007]) ).
thf(1081,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1080]) ).
thf(1099,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1081]) ).
thf(930,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[77,90]) ).
thf(931,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[930]) ).
thf(932,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[931:[bind(A,$thf( I )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( I @ or ) @ ( I @ ( J @ or ) @ implies ) ))]]) ).
thf(985,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[932]) ).
thf(29,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( C @ or ) ) )
| ( C @ ( B @ ( A @ implies ) @ implies ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[20,14]) ).
thf(30,plain,
! [A: $i] : ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[29:[bind(A,$thf( E )),bind(B,$thf( E @ not )),bind(C,$thf( E @ not ))]]) ).
thf(34,plain,
! [A: $i] : ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[30]) ).
thf(1870,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1802,90]) ).
thf(1871,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[1870]) ).
thf(1872,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1871:[bind(A,$thf( F )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( J @ or ) @ ( K @ implies ) @ ( F @ or ) ))]]) ).
thf(1884,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[1872]) ).
thf(185,plain,
! [A: $i] :
( ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( A @ implies ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) ),
inference(rewrite,[status(thm)],[140,181]) ).
thf(291,plain,
! [A: $i] :
( ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(rewrite,[status(thm)],[185,287]) ).
thf(898,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[591,90]) ).
thf(899,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[898]) ).
thf(900,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[899:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ ( H @ or ) @ implies ) @ ( E @ implies ) ))]]) ).
thf(975,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[900]) ).
thf(3384,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ( B != p ) ),
inference(simp,[status(thm)],[1050]) ).
thf(3387,plain,
! [A: $i] :
( ( p @ ( A @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[3384]) ).
thf(1052,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[629,1007]) ).
thf(1053,plain,
! [A: $i] :
( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1052]) ).
thf(1107,plain,
! [A: $i] :
( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1053]) ).
thf(1062,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[90,1007]) ).
thf(1063,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1062]) ).
thf(1092,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1063]) ).
thf(70,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( D @ or ) ) )
| ( B @ ( A @ implies ) @ ( D @ ( C @ or ) @ implies ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[20,16]) ).
thf(71,plain,
! [B: $i,A: $i] : ( A @ ( B @ implies ) @ ( B @ not @ ( A @ or ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[70:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( E @ not ))]]) ).
thf(76,plain,
! [B: $i,A: $i] : ( A @ ( B @ implies ) @ ( B @ not @ ( A @ or ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[71]) ).
thf(68,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( C @ ( D @ or ) @ ( B @ ( A @ implies ) @ implies ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[20,16]) ).
thf(69,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[68:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(75,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[69]) ).
thf(203,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ not @ ( C @ or ) ) )
| ( B @ ( A @ implies ) @ ( C @ ( D @ implies ) @ implies ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[20,75]) ).
thf(204,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ implies ) @ ( A @ not @ ( B @ implies ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[203:[bind(A,$thf( E )),bind(B,$thf( F @ not )),bind(C,$thf( E @ not )),bind(D,$thf( F ))]]) ).
thf(208,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ implies ) @ ( A @ not @ ( B @ implies ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[204]) ).
thf(1727,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1256,107]) ).
thf(1728,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1727]) ).
thf(1729,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1728:[bind(A,$thf( F )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( J @ implies ) @ ( K @ implies ) @ ( F @ or ) ))]]) ).
thf(1801,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1729]) ).
thf(423,plain,
( ( q != q )
| ( r != p )
| ( ( r @ ( q @ implies ) )
!= ( q @ ( p @ implies ) ) ) ),
inference(simp,[status(thm)],[420]) ).
thf(434,plain,
( ( r != p )
| ( ( r @ ( q @ implies ) )
!= ( q @ ( p @ implies ) ) ) ),
inference(simp,[status(thm)],[423]) ).
thf(2565,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ implies ) @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2487,924]) ).
thf(2566,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ implies ) @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2565]) ).
thf(2605,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(simp,[status(thm)],[2566]) ).
thf(1109,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[988,90]) ).
thf(1110,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[1109]) ).
thf(1111,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1110:[bind(A,$thf( F )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( J @ or ) @ ( K @ implies ) @ ( F @ implies ) ))]]) ).
thf(1149,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[1111]) ).
thf(1764,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[595,107]) ).
thf(1765,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1764]) ).
thf(1766,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1765:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ ( H @ or ) @ implies ) @ ( E @ or ) ))]]) ).
thf(1820,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1766]) ).
thf(1767,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[991,107]) ).
thf(1768,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1767]) ).
thf(1769,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1768:[bind(A,$thf( F )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( J @ implies ) @ ( K @ implies ) @ ( F @ implies ) ))]]) ).
thf(1821,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1769]) ).
thf(3645,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( B @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) )
| ~ ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,1796]) ).
thf(3646,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) )
| ~ ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[3645:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(3806,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) )
| ~ ( A @ theorem ) ),
inference(simp,[status(thm)],[3646]) ).
thf(5799,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1256,178]) ).
thf(5800,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[5799]) ).
thf(5801,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( B @ implies ) @ ( C @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[5800:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( I )),bind(D,$thf( I @ ( H @ implies ) @ ( I @ implies ) )),bind(E,$thf( A ))]]) ).
thf(5976,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( B @ implies ) @ ( C @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[5801]) ).
thf(1068,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[77,1007]) ).
thf(1069,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1068]) ).
thf(1102,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1069]) ).
thf(2449,plain,
! [A: $i] :
( ( ( A @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2429,1007]) ).
thf(2450,plain,
! [A: $i] :
( ( A @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[2449]) ).
thf(2481,plain,
! [A: $i] :
( ( A @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[2450]) ).
thf(147,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( E @ ( C @ or ) @ ( D @ or ) ) )
| ( B @ ( A @ implies ) @ ( E @ ( D @ or ) @ ( C @ or ) @ implies ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[20,17]) ).
thf(148,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ implies ) @ ( C @ ( A @ not @ or ) @ ( B @ or ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[147:[bind(A,$thf( F )),bind(B,$thf( H @ ( G @ or ) )),bind(C,$thf( G )),bind(D,$thf( F @ not )),bind(E,$thf( H ))]]) ).
thf(156,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ implies ) @ ( C @ ( A @ not @ or ) @ ( B @ or ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[148]) ).
thf(4209,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ implies ) @ ( C @ ( A @ implies ) @ ( B @ or ) @ implies ) @ axiom ),
inference(rewrite,[status(thm)],[156,20]) ).
thf(1675,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[629,107]) ).
thf(1676,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1675]) ).
thf(1677,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1676:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ not @ ( I @ implies ) @ not @ ( I @ implies ) ))]]) ).
thf(1805,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1677]) ).
thf(1265,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1261,90]) ).
thf(1266,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[1265]) ).
thf(1267,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1266:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ implies ) @ or ) ))]]) ).
thf(1304,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[1267]) ).
thf(2317,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ( B != p ) ),
inference(simp,[status(thm)],[1042]) ).
thf(2318,plain,
! [A: $i] :
( ( p @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[2317]) ).
thf(737,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( D @ or ) ) )
| ( D @ ( B @ ( A @ implies ) @ implies ) @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,595]) ).
thf(738,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[737:[bind(A,$thf( F )),bind(B,$thf( F @ not )),bind(C,$thf( C )),bind(D,$thf( F @ not ))]]) ).
thf(754,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[738]) ).
thf(999,plain,
! [A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[593,924]) ).
thf(1000,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[999]) ).
thf(1049,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(simp,[status(thm)],[1000]) ).
thf(662,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( D @ or ) ) )
| ( D @ ( B @ ( A @ implies ) @ implies ) @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,591]) ).
thf(663,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[662:[bind(A,$thf( F )),bind(B,$thf( F @ not )),bind(C,$thf( C )),bind(D,$thf( F @ not ))]]) ).
thf(690,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[663]) ).
thf(2659,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)],[2420,107]) ).
thf(2660,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)],[2659]) ).
thf(2661,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2660:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ or ) @ or ) ))]]) ).
thf(2678,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2661]) ).
thf(1060,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[595,1007]) ).
thf(1061,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1060]) ).
thf(1098,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1061]) ).
thf(892,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[629,90]) ).
thf(893,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[892]) ).
thf(894,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[893:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ not @ ( I @ implies ) @ not @ ( I @ implies ) ))]]) ).
thf(993,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[894]) ).
thf(60,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( ( B @ ( C @ implies ) )
!= C )
| ~ $true
| ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[47,37]) ).
thf(61,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( ( B @ ( C @ implies ) )
!= C )
| ( B @ theorem ) ),
inference(simp,[status(thm)],[60]) ).
thf(62,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( B @ or ) @ implies ) @ implies ) )
!= ( B @ ( B @ ( B @ or ) @ implies ) ) )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[61:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ ( E @ ( E @ or ) @ implies ) ))]]) ).
thf(67,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( B @ or ) @ implies ) @ implies ) )
!= ( B @ ( B @ ( B @ or ) @ implies ) ) )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[62]) ).
thf(5866,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[595,178]) ).
thf(5867,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[5866]) ).
thf(5868,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ ( B @ or ) @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[5867:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( F @ ( F @ ( F @ or ) @ implies ) )),bind(D,$thf( A ))]]) ).
thf(5995,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ ( B @ or ) @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[5868]) ).
thf(52,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47,13]) ).
thf(53,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[52]) ).
thf(63,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) ) ),
inference(simp,[status(thm)],[53]) ).
thf(117,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( C @ or ) ) )
| ( ( C @ ( B @ ( A @ implies ) @ implies ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,63]) ).
thf(118,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) ) ),
inference(pattern_uni,[status(thm)],[117:[bind(A,$thf( E )),bind(B,$thf( E @ not )),bind(C,$thf( E @ not ))]]) ).
thf(120,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) ) ),
inference(simp,[status(thm)],[118]) ).
thf(544,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[120,181,287]) ).
thf(3385,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( B @ ( A @ implies ) @ ( D @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,1050]) ).
thf(3386,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(pattern_uni,[status(thm)],[3385:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(3388,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(simp,[status(thm)],[3386]) ).
thf(2865,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2611,107]) ).
thf(2866,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2865]) ).
thf(2867,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2866:[bind(A,$thf( F )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( K @ implies ) @ ( H @ implies ) @ ( F @ or ) ))]]) ).
thf(2885,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2867]) ).
thf(1678,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[988,107]) ).
thf(1679,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1678]) ).
thf(1680,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1679:[bind(A,$thf( F )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( J @ or ) @ ( K @ implies ) @ ( F @ implies ) ))]]) ).
thf(1807,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1680]) ).
thf(1064,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[591,1007]) ).
thf(1065,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1064]) ).
thf(1101,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1065]) ).
thf(151,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ implies ) @ axiom )
!= ( D @ axiom ) )
| ~ $true
| ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[17,22]) ).
thf(152,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ or ) @ implies ) @ axiom )
!= ( D @ axiom ) )
| ( D @ theorem ) ),
inference(simp,[status(thm)],[151]) ).
thf(153,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ ( B @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[152:[bind(A,$thf( M )),bind(B,$thf( K )),bind(C,$thf( N )),bind(D,$thf( N @ ( M @ or ) @ ( K @ or ) @ ( N @ ( K @ or ) @ ( M @ or ) @ implies ) ))]]) ).
thf(158,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ ( B @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[153]) ).
thf(2805,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2551,90]) ).
thf(2806,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2805]) ).
thf(2807,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ or ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2806:[bind(A,$thf( F )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( K @ implies ) @ ( H @ or ) @ ( F @ implies ) ))]]) ).
thf(2823,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ or ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2807]) ).
thf(2662,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2420,90]) ).
thf(2663,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2662]) ).
thf(2664,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2663:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ or ) @ or ) ))]]) ).
thf(2680,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2664]) ).
thf(116,plain,
! [A: $i] :
( ( A
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) )
| ( ( A @ ( A @ or ) )
!= ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) ) ) ),
inference(simp,[status(thm)],[63]) ).
thf(119,plain,
( ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ equivalent ) @ ( p @ implies ) @ or ) )
!= ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) ) ),
inference(simp,[status(thm)],[116]) ).
thf(121,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ equivalent ) @ ( p @ implies ) @ or ) ) )
| ( ( B @ ( A @ implies ) )
!= ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,119]) ).
thf(122,plain,
! [B: $i,A: $i] :
( ( B
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) )
| ( ( A @ not )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) )
| ( ( B @ ( A @ implies ) )
!= ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) ) ) ),
inference(simp,[status(thm)],[121]) ).
thf(123,plain,
! [A: $i] :
( ( ( A @ not )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) )
| ( ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( A @ implies ) )
!= ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) ) ) ),
inference(simp,[status(thm)],[122]) ).
thf(269,plain,
! [A: $i] :
( ( ( A @ not )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) )
| ( ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( A @ implies ) )
!= ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ) ),
inference(rewrite,[status(thm)],[123,181]) ).
thf(270,plain,
! [A: $i] :
( ( ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not )
!= ( A @ not ) )
| ( ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( A @ implies ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) )
| ( ( A @ not )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[269]) ).
thf(271,plain,
! [A: $i] :
( ( ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not )
!= ( A @ not ) )
| ( ( r @ ( q @ equivalent ) @ ( p @ implies ) )
!= ( r @ ( q @ equivalent ) ) )
| ( A != p )
| ( ( A @ not )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) ) ),
inference(simp,[status(thm)],[270]) ).
thf(276,plain,
( ( ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not )
!= ( p @ not ) )
| ( ( r @ ( q @ equivalent ) @ ( p @ implies ) )
!= ( r @ ( q @ equivalent ) ) )
| ( ( r @ ( q @ equivalent ) @ ( p @ implies ) )
!= ( p @ not ) ) ),
inference(simp,[status(thm)],[271]) ).
thf(1607,plain,
( ( ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not )
!= ( p @ not ) )
| ( ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) )
| ( ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) )
!= ( p @ not ) ) ),
inference(rewrite,[status(thm)],[276,287]) ).
thf(5193,plain,
! [B: $i,A: $i] :
( ( ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) )
!= B )
| ( ( B @ ( A @ implies ) )
!= ( p @ not ) ) ),
inference(simp,[status(thm)],[5192]) ).
thf(5194,plain,
! [A: $i] :
( ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ ( A @ implies ) )
!= ( p @ not ) ),
inference(simp,[status(thm)],[5193]) ).
thf(417,plain,
( ( r != q )
| ( r != q )
| ( ( r @ ( q @ implies ) )
!= ( q @ ( p @ implies ) ) ) ),
inference(simp,[status(thm)],[304]) ).
thf(432,plain,
( ( r != q )
| ( ( r @ ( q @ implies ) )
!= ( q @ ( p @ implies ) ) ) ),
inference(simp,[status(thm)],[417]) ).
thf(36,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) @ theorem )
!= ( B @ theorem ) )
| ~ ( B @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[35]) ).
thf(1070,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[64,1007]) ).
thf(1071,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1070]) ).
thf(1097,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1071]) ).
thf(164,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[77,13]) ).
thf(165,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[164]) ).
thf(175,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) ) ),
inference(simp,[status(thm)],[165]) ).
thf(5283,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) @ ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[175,181,287]) ).
thf(95,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,13]) ).
thf(96,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[95]) ).
thf(106,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ ( q @ ( p @ implies ) @ and ) @ implies ) ) ),
inference(simp,[status(thm)],[96]) ).
thf(278,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) @ ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[106,181]) ).
thf(279,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) )
| ( B
!= ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[278]) ).
thf(282,plain,
! [A: $i] :
( ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( A @ or ) )
!= ( r @ ( q @ equivalent ) @ ( p @ implies ) ) ),
inference(simp,[status(thm)],[279]) ).
thf(294,plain,
! [A: $i] :
( ( r @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( A @ or ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not @ ( p @ implies ) ) ),
inference(rewrite,[status(thm)],[282,287]) ).
thf(126,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( B @ ( C @ implies ) @ theorem ) )
| ~ ( C @ theorem )
| ~ $true
| ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[64,24]) ).
thf(127,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( B @ ( C @ implies ) @ theorem ) )
| ~ ( C @ theorem )
| ( B @ theorem ) ),
inference(simp,[status(thm)],[126]) ).
thf(128,plain,
! [A: $i] :
( ~ ( A @ not @ ( A @ implies ) @ theorem )
| ( A @ not @ theorem ) ),
inference(pattern_uni,[status(thm)],[127:[bind(A,$thf( G )),bind(B,$thf( G @ not )),bind(C,$thf( G @ not @ ( G @ implies ) ))]]) ).
thf(136,plain,
! [A: $i] :
( ~ ( A @ not @ ( A @ implies ) @ theorem )
| ( A @ not @ theorem ) ),
inference(simp,[status(thm)],[128]) ).
thf(1781,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1261,107]) ).
thf(1782,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1781]) ).
thf(1783,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1782:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ implies ) @ or ) ))]]) ).
thf(1829,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1783]) ).
thf(1604,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( B @ ( A @ implies ) @ ( D @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ) ),
inference(paramod_ordered,[status(thm)],[20,1096]) ).
thf(1605,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(pattern_uni,[status(thm)],[1604:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(1606,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ ( r @ implies ) @ not @ ( r @ ( q @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1605]) ).
thf(2734,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2550,107]) ).
thf(2735,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[2734]) ).
thf(2736,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ or ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2735:[bind(A,$thf( F )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( K @ ( K @ implies ) @ ( H @ or ) @ ( F @ or ) ))]]) ).
thf(2754,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( D @ implies ) @ ( C @ or ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2736]) ).
thf(56703,plain,
$false,
inference(e,[status(thm)],[1185,2822,629,2612,138,2427,2544,977,1882,2953,2671,247,1142,3382,2686,4839,5192,1095,24,2886,37,25,14,2755,1264,1826,2488,20,421,6071,2420,924,1302,179,591,1828,3152,1183,1796,1351,988,307,292,1042,297,33,21,137,92,5983,65,1296,1819,889,224,1106,2115,980,1096,593,109,77,5992,2551,6097,2487,1050,2482,1099,985,34,64,296,17,176,1007,1884,22,291,1256,27,975,3387,12,1107,49,1092,181,6061,2478,76,208,1801,434,2605,858,91,66,1149,108,1820,1821,594,3806,5976,1102,1044,2550,2481,4209,1805,1304,2318,754,1049,48,690,295,18,2678,1098,993,67,177,16,2429,5995,2486,544,1802,3388,1797,595,991,2885,2611,1807,304,1101,158,2823,23,75,2680,1607,5194,287,432,36,1097,19,107,5990,5283,294,136,1829,1261,47,15,178,90,1606,2754]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL335-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.07 % 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.11/0.38 % Computer : n002.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Fri Sep 25 22:19:35 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.84/0.84 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.07/1.03 % [INFO] Parsing done (186ms).
% 1.07/1.04 % [INFO] Running in sequential loop mode.
% 2.15/1.40 % [INFO] eprover registered as external prover.
% 2.15/1.41 % [INFO] Scanning for conjecture ...
% 2.15/1.48 % [INFO] Found a conjecture (or negated_conjecture) and 10 axioms. Running axiom selection ...
% 2.41/1.51 % [INFO] Axiom selection finished. Selected 10 axioms (removed 0 axioms).
% 2.41/1.53 % [INFO] Problem is propositional (TPTP CNF).
% 2.41/1.54 % [INFO] Type checking passed.
% 2.41/1.54 % [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 ...
% 260.27/74.09 % External prover 'e' found a proof!
% 260.27/74.10 % [INFO] Killing All external provers ...
% 260.27/74.10 % Time passed: 73614ms (effective reasoning time: 73051ms)
% 260.27/74.10 % Axioms used in derivation (10): axiom_1_5, equivalent_defn, and_defn, axiom_1_4, rule_1, axiom_1_3, implies_definition, axiom_1_2, rule_2, axiom_1_6
% 260.27/74.10 % No. of inferences in proof: 560
% 260.27/74.10 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 73614 ms resp. 73051 ms w/o parsing
% 259.04/74.22 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 259.04/74.23 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------