%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LCL319-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 : n008.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:30 AM UTC 2026
% Result : Unsatisfiable 199.88s 55.10s
% Output : Refutation 201.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 11
% Syntax : Number of formulae : 452 ( 216 unt; 0 typ; 0 def)
% Number of atoms : 1151 ( 363 equ; 0 cnn)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 5907 ( 518 ~; 355 |; 0 &;5034 @)
% ( 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 : 12 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 1199 ( 0 ^;1199 !; 0 ?;1199 :)
% 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(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(1,negated_conjecture,
~ ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) @ theorem ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
thf(12,plain,
~ ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) @ theorem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(13,plain,
~ ( q @ ( p @ equivalent ) @ ( q @ ( p @ 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(179,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ and ) )
= ( B @ not @ ( A @ implies ) @ not ) ),
inference(rewrite,[status(thm)],[26,20]) ).
thf(181,plain,
~ ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ),
inference(rewrite,[status(thm)],[13,179]) ).
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(278,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ equivalent ) )
= ( A @ ( B @ implies ) @ not @ ( B @ ( A @ implies ) @ implies ) @ not ) ),
inference(rewrite,[status(thm)],[28,179]) ).
thf(281,plain,
~ ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ),
inference(rewrite,[status(thm)],[181,278]) ).
thf(856,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[90,281]) ).
thf(857,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[856]) ).
thf(858,plain,
~ ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[857:[bind(A,$thf( q @ not @ ( p @ implies ) @ not )),bind(B,$thf( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ))]]) ).
thf(942,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[90,858]) ).
thf(943,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[942]) ).
thf(956,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[943]) ).
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(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(1645,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(1646,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)],[1645]) ).
thf(1647,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1646:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ or ) @ ( H @ implies ) ))]]) ).
thf(1793,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1647]) ).
thf(1833,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)],[1793,107]) ).
thf(1834,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)],[1833]) ).
thf(1835,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1834:[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(1846,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1835]) ).
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(158,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(159,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[158:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( E @ not ))]]) ).
thf(178,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[159]) ).
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(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)],[178,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(587,plain,
! [A: $i] : ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[580]) ).
thf(833,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)],[587,90]) ).
thf(834,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[833]) ).
thf(835,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[834:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( H @ ( H @ or ) @ not @ ( H @ or ) ))]]) ).
thf(892,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[835]) ).
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(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(1213,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)],[178,91]) ).
thf(1214,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)],[1213]) ).
thf(1215,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1214:[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(1237,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[1215]) ).
thf(818,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(819,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)],[818]) ).
thf(820,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[819:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ or ) @ ( H @ implies ) ))]]) ).
thf(903,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[820]) ).
thf(1024,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)],[903,90]) ).
thf(1025,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)],[1024]) ).
thf(1026,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1025:[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(1031,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[1026]) ).
thf(1714,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[107,858]) ).
thf(1715,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1714]) ).
thf(1763,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1715]) ).
thf(1986,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( B @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,1763]) ).
thf(1987,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[1986:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(2062,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( A @ theorem ) ),
inference(simp,[status(thm)],[1987]) ).
thf(573,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(574,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)],[573]) ).
thf(575,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[574:[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)],[575]) ).
thf(718,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(719,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[718:[bind(A,$thf( F )),bind(B,$thf( F @ not )),bind(C,$thf( C )),bind(D,$thf( F @ not ))]]) ).
thf(741,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[719]) ).
thf(912,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,858]) ).
thf(913,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[912]) ).
thf(945,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[913]) ).
thf(1039,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( B @ ( A @ implies ) @ ( D @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ) ),
inference(paramod_ordered,[status(thm)],[20,945]) ).
thf(1040,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(pattern_uni,[status(thm)],[1039:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(1041,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1040]) ).
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(223,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(224,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)],[223]) ).
thf(225,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ implies ) @ ( C @ ( A @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[224:[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(226,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ implies ) @ ( C @ ( A @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[225]) ).
thf(1203,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)],[226,91]) ).
thf(1204,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)],[1203]) ).
thf(1205,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( A @ or ) @ ( C @ ( A @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1204:[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(1233,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( A @ or ) @ ( C @ ( A @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[1205]) ).
thf(162,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[77,13]) ).
thf(163,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[162]) ).
thf(173,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) ) ),
inference(simp,[status(thm)],[163]) ).
thf(492,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[173,179,278]) ).
thf(493,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ( ( A @ ( B @ or ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[492]) ).
thf(696,plain,
! [B: $i,A: $i] :
( ( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not )
!= ( q @ not @ ( p @ implies ) @ not ) )
| ( ( B @ ( A @ or ) )
!= ( A @ ( B @ or ) ) )
| ( ( A @ ( B @ or ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(eqfactor_ordered,[status(thm)],[493]) ).
thf(699,plain,
! [B: $i,A: $i] :
( ( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) )
!= ( q @ not @ ( p @ implies ) ) )
| ( B != A )
| ( A != B )
| ( ( A @ ( B @ or ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[696]) ).
thf(703,plain,
! [A: $i] :
( ( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) )
!= ( q @ not @ ( p @ implies ) ) )
| ( ( A @ ( A @ or ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[699]) ).
thf(803,plain,
! [A: $i] :
( ( ( p @ ( q @ implies ) @ not )
!= ( q @ not ) )
| ( ( q @ ( p @ implies ) )
!= p )
| ( ( A @ ( A @ or ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[703]) ).
thf(807,plain,
! [A: $i] :
( ( ( p @ ( q @ implies ) )
!= q )
| ( ( q @ ( p @ implies ) )
!= p )
| ( ( A @ ( A @ or ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[803]) ).
thf(812,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( C @ or ) ) )
| ( ( p @ ( q @ implies ) )
!= q )
| ( ( q @ ( p @ implies ) )
!= p )
| ( ( B @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(paramod_ordered,[status(thm)],[20,807]) ).
thf(813,plain,
! [A: $i] :
( ( ( p @ ( q @ implies ) )
!= q )
| ( ( q @ ( p @ implies ) )
!= p )
| ( ( A @ not @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(pattern_uni,[status(thm)],[812:[bind(A,$thf( E )),bind(B,$thf( E @ not )),bind(C,$thf( E @ not ))]]) ).
thf(814,plain,
! [A: $i] :
( ( ( p @ ( q @ implies ) )
!= q )
| ( ( q @ ( p @ implies ) )
!= p )
| ( ( A @ not @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[813]) ).
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(174,plain,
! [B: $i,A: $i] : ( A @ ( B @ implies ) @ ( B @ not @ ( A @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[161]) ).
thf(236,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,174]) ).
thf(237,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ implies ) @ ( B @ not @ ( A @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[236:[bind(A,$thf( E )),bind(B,$thf( F @ not )),bind(C,$thf( E @ not )),bind(D,$thf( F ))]]) ).
thf(253,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ implies ) @ ( B @ not @ ( A @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[237]) ).
thf(563,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)],[253,66]) ).
thf(564,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)],[563]) ).
thf(565,plain,
! [A: $i] : ( A @ not @ ( A @ not @ or ) @ not @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[564:[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(588,plain,
! [A: $i] : ( A @ not @ ( A @ not @ or ) @ not @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[565]) ).
thf(625,plain,
! [A: $i] : ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem ),
inference(rewrite,[status(thm)],[588,20]) ).
thf(1688,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)],[625,107]) ).
thf(1689,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)],[1688]) ).
thf(1690,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1689:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ not @ ( I @ implies ) @ not @ ( I @ implies ) ))]]) ).
thf(1782,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1690]) ).
thf(2057,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[90,1763]) ).
thf(2058,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2057]) ).
thf(2059,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( A @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( C @ theorem ) ),
inference(pattern_uni,[status(thm)],[2058:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( F @ ( E @ implies ) ))]]) ).
thf(2067,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( A @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( C @ theorem ) ),
inference(simp,[status(thm)],[2059]) ).
thf(697,plain,
! [B: $i,A: $i] :
( ( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not )
!= ( q @ not @ ( p @ implies ) @ not ) )
| ( B != A )
| ( A != B )
| ( ( A @ ( B @ or ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[696]) ).
thf(702,plain,
! [A: $i] :
( ( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not )
!= ( q @ not @ ( p @ implies ) @ not ) )
| ( ( A @ ( A @ or ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[697]) ).
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(145,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( E @ ( D @ or ) ) )
| ( E @ ( C @ or ) @ ( D @ or ) @ ( B @ ( A @ implies ) @ ( C @ or ) @ implies ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[20,17]) ).
thf(146,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( B @ or ) @ ( C @ not @ or ) @ ( A @ ( C @ implies ) @ ( B @ or ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[145:[bind(A,$thf( F )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( F @ not )),bind(E,$thf( B ))]]) ).
thf(153,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( B @ or ) @ ( C @ not @ or ) @ ( A @ ( C @ implies ) @ ( B @ or ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[146]) ).
thf(4788,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( B @ or ) @ ( C @ implies ) @ ( A @ ( C @ implies ) @ ( B @ or ) @ implies ) @ axiom ),
inference(rewrite,[status(thm)],[153,20]) ).
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(2365,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)],[178,108]) ).
thf(2366,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)],[2365]) ).
thf(2367,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2366:[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(2403,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[2367]) ).
thf(191,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,181]) ).
thf(192,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[191]) ).
thf(195,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(simp,[status(thm)],[192]) ).
thf(325,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[195,278]) ).
thf(3229,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( C @ or ) ) )
| ( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not )
!= ( q @ not @ ( p @ implies ) @ not ) )
| ( ( B @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(paramod_ordered,[status(thm)],[20,702]) ).
thf(3230,plain,
! [A: $i] :
( ( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not )
!= ( q @ not @ ( p @ implies ) @ not ) )
| ( ( A @ not @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(pattern_uni,[status(thm)],[3229:[bind(A,$thf( E )),bind(B,$thf( E @ not )),bind(C,$thf( E @ not ))]]) ).
thf(3231,plain,
! [A: $i] :
( ( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not )
!= ( q @ not @ ( p @ implies ) @ not ) )
| ( ( A @ not @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[3230]) ).
thf(804,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( C @ or ) ) )
| ( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) )
!= ( q @ not @ ( p @ implies ) ) )
| ( ( B @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(paramod_ordered,[status(thm)],[20,703]) ).
thf(805,plain,
! [A: $i] :
( ( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) )
!= ( q @ not @ ( p @ implies ) ) )
| ( ( A @ not @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(pattern_uni,[status(thm)],[804:[bind(A,$thf( E )),bind(B,$thf( E @ not )),bind(C,$thf( E @ not ))]]) ).
thf(806,plain,
! [A: $i] :
( ( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) )
!= ( q @ not @ ( p @ implies ) ) )
| ( ( A @ not @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[805]) ).
thf(883,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[178,90]) ).
thf(884,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[883]) ).
thf(885,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( B @ or ) @ ( B @ ( C @ implies ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[884:[bind(A,$thf( I )),bind(B,$thf( K )),bind(C,$thf( C )),bind(D,$thf( K @ not @ ( I @ or ) @ ( I @ ( K @ implies ) @ implies ) ))]]) ).
thf(905,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( B @ or ) @ ( B @ ( C @ implies ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[885]) ).
thf(808,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( C @ or ) ) )
| ( ( p @ ( q @ implies ) @ not )
!= ( q @ not ) )
| ( ( q @ ( p @ implies ) )
!= p )
| ( ( B @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(paramod_ordered,[status(thm)],[20,803]) ).
thf(809,plain,
! [A: $i] :
( ( ( p @ ( q @ implies ) @ not )
!= ( q @ not ) )
| ( ( q @ ( p @ implies ) )
!= p )
| ( ( A @ not @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(pattern_uni,[status(thm)],[808:[bind(A,$thf( E )),bind(B,$thf( E @ not )),bind(C,$thf( E @ not ))]]) ).
thf(810,plain,
! [A: $i] :
( ( ( p @ ( q @ implies ) @ not )
!= ( q @ not ) )
| ( ( q @ ( p @ implies ) )
!= p )
| ( ( A @ not @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[809]) ).
thf(2048,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[107,1763]) ).
thf(2049,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2048]) ).
thf(2050,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( C @ theorem ) ),
inference(pattern_uni,[status(thm)],[2049:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( F @ ( E @ or ) ))]]) ).
thf(2061,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( C @ theorem ) ),
inference(simp,[status(thm)],[2050]) ).
thf(918,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[591,858]) ).
thf(919,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[918]) ).
thf(952,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[919]) ).
thf(556,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(557,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)],[556]) ).
thf(558,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[557:[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(590,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[558]) ).
thf(926,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[590,858]) ).
thf(927,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[926]) ).
thf(957,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[927]) ).
thf(836,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(837,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)],[836]) ).
thf(838,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[837:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ ( H @ or ) @ implies ) @ ( E @ implies ) ))]]) ).
thf(894,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[838]) ).
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(2346,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)],[226,108]) ).
thf(2347,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)],[2346]) ).
thf(2348,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2347:[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(2396,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[2348]) ).
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(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(1096,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[90,956]) ).
thf(1097,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1096]) ).
thf(1098,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( C @ theorem ) ),
inference(pattern_uni,[status(thm)],[1097:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( F @ ( E @ implies ) ))]]) ).
thf(1106,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( C @ theorem ) ),
inference(simp,[status(thm)],[1098]) ).
thf(1174,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(1175,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)],[1174]) ).
thf(1176,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1175:[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(1234,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1176]) ).
thf(924,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[77,858]) ).
thf(925,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[924]) ).
thf(948,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[925]) ).
thf(868,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(869,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)],[868]) ).
thf(870,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[869:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ implies ) @ ( H @ implies ) ))]]) ).
thf(895,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[870]) ).
thf(974,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[895,858]) ).
thf(975,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[974]) ).
thf(989,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[975]) ).
thf(1254,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1237,858]) ).
thf(1255,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1254]) ).
thf(1270,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ implies ) @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1255]) ).
thf(1671,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)],[587,107]) ).
thf(1672,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[1671]) ).
thf(1673,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1672:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( H @ ( H @ or ) @ not @ ( H @ or ) ))]]) ).
thf(1772,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1673]) ).
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(2441,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)],[2403,107]) ).
thf(2442,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)],[2441]) ).
thf(2443,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2442:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ or ) @ or ) ))]]) ).
thf(2460,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2443]) ).
thf(847,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(848,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)],[847]) ).
thf(849,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[848:[bind(A,$thf( I )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( I @ or ) @ ( I @ ( J @ or ) @ implies ) ))]]) ).
thf(901,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[849]) ).
thf(2425,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2403,858]) ).
thf(2426,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[2425]) ).
thf(2455,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ or ) @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[2426]) ).
thf(1642,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[107,956]) ).
thf(1643,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( ( D @ ( C @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1642]) ).
thf(1644,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( C @ theorem ) ),
inference(pattern_uni,[status(thm)],[1643:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( C )),bind(D,$thf( F @ ( E @ or ) ))]]) ).
thf(1791,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ~ ( C @ theorem ) ),
inference(simp,[status(thm)],[1644]) ).
thf(52,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47,13]) ).
thf(53,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[52]) ).
thf(63,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ 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 ) )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,63]) ).
thf(118,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ 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 ) )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) ) ),
inference(simp,[status(thm)],[118]) ).
thf(275,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[120,179]) ).
thf(276,plain,
! [A: $i] :
( ( ( A @ not )
!= ( q @ ( p @ equivalent ) ) )
| ( ( A @ not @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[275]) ).
thf(457,plain,
! [A: $i] :
( ( ( A @ not )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) )
| ( ( A @ not @ ( A @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(rewrite,[status(thm)],[276,278]) ).
thf(1676,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(1677,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)],[1676]) ).
thf(1678,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1677:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ ( H @ or ) @ implies ) @ ( E @ implies ) ))]]) ).
thf(1776,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1678]) ).
thf(985,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)],[895,90]) ).
thf(986,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)],[985]) ).
thf(987,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[986:[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(997,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[987]) ).
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)],[1237,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(1278,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[1267]) ).
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(850,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)],[590,90]) ).
thf(851,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)],[850]) ).
thf(852,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[851:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ ( H @ or ) @ implies ) @ ( E @ or ) ))]]) ).
thf(904,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[852]) ).
thf(938,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47,858]) ).
thf(939,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[938]) ).
thf(958,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[939]) ).
thf(1648,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)],[903,107]) ).
thf(1649,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)],[1648]) ).
thf(1650,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1649:[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(1795,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1650]) ).
thf(1691,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)],[1234,107]) ).
thf(1692,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)],[1691]) ).
thf(1693,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1692:[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(1784,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1693]) ).
thf(1694,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(1695,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)],[1694]) ).
thf(1696,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1695:[bind(A,$thf( I )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( I @ or ) @ ( I @ ( J @ or ) @ implies ) ))]]) ).
thf(1786,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1696]) ).
thf(1712,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[107,281]) ).
thf(1713,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1712]) ).
thf(1765,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[1713]) ).
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(147,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(148,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)],[147:[bind(A,$thf( F )),bind(B,$thf( H @ ( G @ or ) )),bind(C,$thf( F @ not )),bind(D,$thf( G )),bind(E,$thf( H ))]]) ).
thf(154,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( A @ not @ or ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ implies ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[148]) ).
thf(4805,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( A @ implies ) @ ( B @ or ) @ ( C @ ( B @ or ) @ ( A @ implies ) @ implies ) @ axiom ),
inference(rewrite,[status(thm)],[154,20]) ).
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(149,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(150,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)],[149]) ).
thf(151,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ ( B @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[150:[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(155,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ ( B @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[151]) ).
thf(1013,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[903,858]) ).
thf(1014,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1013]) ).
thf(1029,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1014]) ).
thf(934,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,858]) ).
thf(935,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[934]) ).
thf(959,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[935]) ).
thf(189,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[64,181]) ).
thf(190,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[189]) ).
thf(199,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(simp,[status(thm)],[190]) ).
thf(490,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[199,278]) ).
thf(570,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)],[226,66]) ).
thf(571,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)],[570]) ).
thf(572,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ ( A @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[571:[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(589,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ ( A @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[572]) ).
thf(666,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,590]) ).
thf(667,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[666:[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 @ or ) @ theorem ),
inference(simp,[status(thm)],[667]) ).
thf(78,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,13]) ).
thf(79,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[78]) ).
thf(89,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(139,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) )
!= ( q @ ( p @ equivalent ) ) )
| ( B
!= ( q @ ( p @ and ) ) ) ),
inference(simp,[status(thm)],[89]) ).
thf(140,plain,
! [A: $i] :
( ( q @ ( p @ and ) @ ( A @ implies ) )
!= ( q @ ( p @ equivalent ) ) ),
inference(simp,[status(thm)],[139]) ).
thf(182,plain,
! [A: $i] :
( ( q @ not @ ( p @ implies ) @ not @ ( A @ implies ) )
!= ( q @ ( p @ equivalent ) ) ),
inference(rewrite,[status(thm)],[140,179]) ).
thf(282,plain,
! [A: $i] :
( ( q @ not @ ( p @ implies ) @ not @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(rewrite,[status(thm)],[182,278]) ).
thf(928,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[64,858]) ).
thf(929,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[928]) ).
thf(954,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[929]) ).
thf(1720,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)],[895,107]) ).
thf(1721,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)],[1720]) ).
thf(1722,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1721:[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(1798,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1722]) ).
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(247,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) @ ( B @ not @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[174,181]) ).
thf(248,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( B @ not @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[247]) ).
thf(249,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( B @ not @ ( A @ or ) @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(simp,[status(thm)],[248]) ).
thf(544,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( B @ not @ ( A @ or ) @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[249,278]) ).
thf(1300,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1234,858]) ).
thf(1301,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1300]) ).
thf(1317,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1301]) ).
thf(1654,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)],[1237,107]) ).
thf(1655,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)],[1654]) ).
thf(1656,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1655:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ implies ) @ or ) ))]]) ).
thf(1797,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1656]) ).
thf(116,plain,
! [A: $i] :
( ( A
!= ( q @ ( p @ equivalent ) ) )
| ( ( A @ ( A @ or ) )
!= ( q @ ( p @ and ) ) ) ),
inference(simp,[status(thm)],[63]) ).
thf(119,plain,
( ( q @ ( p @ equivalent ) @ ( q @ ( p @ equivalent ) @ or ) )
!= ( q @ ( p @ and ) ) ),
inference(simp,[status(thm)],[116]) ).
thf(183,plain,
( ( q @ ( p @ equivalent ) @ ( q @ ( p @ equivalent ) @ or ) )
!= ( q @ not @ ( p @ implies ) @ not ) ),
inference(rewrite,[status(thm)],[119,179]) ).
thf(284,plain,
( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ or ) )
!= ( q @ not @ ( p @ implies ) @ not ) ),
inference(rewrite,[status(thm)],[183,278]) ).
thf(314,plain,
( ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ implies ) )
!= ( q @ not @ ( p @ implies ) @ not ) ),
inference(rewrite,[status(thm)],[284,20]) ).
thf(1822,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1793,858]) ).
thf(1823,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[1822]) ).
thf(1839,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[1823]) ).
thf(184,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[63,179]) ).
thf(319,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[184,278]) ).
thf(916,plain,
! [A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[587,858]) ).
thf(917,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[916]) ).
thf(946,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[917]) ).
thf(2444,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)],[2403,90]) ).
thf(2445,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)],[2444]) ).
thf(2446,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2445:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ or ) @ or ) ))]]) ).
thf(2462,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2446]) ).
thf(844,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)],[625,90]) ).
thf(845,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)],[844]) ).
thf(846,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[845:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ not @ ( I @ implies ) @ not @ ( I @ implies ) ))]]) ).
thf(899,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[846]) ).
thf(265,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[178,181]) ).
thf(266,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[265]) ).
thf(267,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(simp,[status(thm)],[266]) ).
thf(549,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[267,278]) ).
thf(180,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[89,179]) ).
thf(315,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[180,278]) ).
thf(36,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) @ theorem )
!= ( B @ theorem ) )
| ~ ( B @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[35]) ).
thf(2600,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( D @ not @ ( B @ ( A @ implies ) @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ) ),
inference(paramod_ordered,[status(thm)],[20,2455]) ).
thf(2601,plain,
! [B: $i,A: $i] :
( ( A @ not @ ( A @ ( B @ implies ) @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(pattern_uni,[status(thm)],[2600:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(2604,plain,
! [B: $i,A: $i] :
( ( A @ not @ ( A @ ( B @ implies ) @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[2601]) ).
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(1700,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)],[590,107]) ).
thf(1701,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)],[1700]) ).
thf(1702,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1701:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ ( H @ or ) @ implies ) @ ( E @ or ) ))]]) ).
thf(1789,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1702]) ).
thf(922,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[625,858]) ).
thf(923,plain,
! [A: $i] :
( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ theorem ) ),
inference(simp,[status(thm)],[922]) ).
thf(960,plain,
! [A: $i] :
( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[923]) ).
thf(95,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,13]) ).
thf(96,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[95]) ).
thf(106,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ ( p @ and ) @ implies ) ) ),
inference(simp,[status(thm)],[96]) ).
thf(210,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[106,179]) ).
thf(211,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( q @ ( p @ equivalent ) ) )
| ( B
!= ( q @ not @ ( p @ implies ) @ not ) ) ),
inference(simp,[status(thm)],[210]) ).
thf(214,plain,
! [A: $i] :
( ( q @ not @ ( p @ implies ) @ not @ ( A @ or ) )
!= ( q @ ( p @ equivalent ) ) ),
inference(simp,[status(thm)],[211]) ).
thf(283,plain,
! [A: $i] :
( ( q @ not @ ( p @ implies ) @ not @ ( A @ or ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not ) ),
inference(rewrite,[status(thm)],[214,278]) ).
thf(1311,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)],[1234,90]) ).
thf(1312,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)],[1311]) ).
thf(1313,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1312:[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(1320,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[1313]) ).
thf(1836,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)],[1793,90]) ).
thf(1837,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)],[1836]) ).
thf(1838,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1837:[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(1848,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[1838]) ).
thf(212,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( B @ ( A @ implies ) @ ( D @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,210]) ).
thf(213,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(pattern_uni,[status(thm)],[212:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(215,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ ( p @ equivalent ) @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(simp,[status(thm)],[213]) ).
thf(454,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( p @ ( q @ implies ) @ not @ ( q @ ( p @ implies ) @ implies ) @ not @ ( q @ not @ ( p @ implies ) @ not @ implies ) ) ),
inference(rewrite,[status(thm)],[215,278]) ).
thf(44367,plain,
$false,
inference(e,[status(thm)],[956,1846,892,138,1237,1031,2062,741,1793,1041,1233,814,945,174,1782,24,2067,37,25,14,587,702,4788,2403,20,325,3231,492,179,591,253,806,905,810,2061,952,957,894,21,137,2396,33,92,65,625,493,1106,1234,948,989,1270,1772,109,2460,77,901,2455,1791,590,457,1776,997,1278,34,64,17,904,958,1795,281,27,22,1784,12,1786,49,1765,76,4805,208,858,91,66,155,108,1029,895,959,278,226,490,589,690,18,282,954,1798,48,67,16,544,1317,1763,703,1797,314,1839,903,319,946,23,75,2462,899,549,315,36,2604,19,107,136,807,1789,960,283,47,15,178,90,803,1320,1848,454]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL319-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.11 % 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.22/0.48 % Computer : n008.cluster.edu
% 0.22/0.48 % Model : x86_64 x86_64
% 0.22/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.48 % Memory : 8046.5625MB
% 0.22/0.48 % OS : Linux 6.8.0-71-generic
% 0.22/0.48 % CPULimit : 300
% 0.22/0.48 % WCLimit : 300
% 0.22/0.48 % DateTime : Fri Sep 25 22:15:54 UTC 2026
% 0.22/0.48 % CPUTime :
% 0.22/0.48 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.33/1.22 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.88/1.52 % [INFO] Parsing done (295ms).
% 1.88/1.54 % [INFO] Running in sequential loop mode.
% 2.65/2.05 % [INFO] eprover registered as external prover.
% 2.93/2.06 % [INFO] Scanning for conjecture ...
% 3.14/2.18 % [INFO] Found a conjecture (or negated_conjecture) and 10 axioms. Running axiom selection ...
% 3.21/2.23 % [INFO] Axiom selection finished. Selected 10 axioms (removed 0 axioms).
% 3.21/2.26 % [INFO] Problem is propositional (TPTP CNF).
% 3.21/2.27 % [INFO] Type checking passed.
% 3.21/2.27 % [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 ...
% 199.88/55.09 % External prover 'e' found a proof!
% 199.88/55.09 % [INFO] Killing All external provers ...
% 199.88/55.10 % Time passed: 54406ms (effective reasoning time: 53542ms)
% 199.88/55.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
% 199.88/55.10 % No. of inferences in proof: 452
% 199.88/55.10 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 54406 ms resp. 53542 ms w/o parsing
% 201.80/55.41 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 201.80/55.42 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------