%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LCL266-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 : n011.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:24 AM UTC 2026
% Result : Unsatisfiable 128.13s 39.05s
% Output : Refutation 130.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 11
% Syntax : Number of formulae : 788 ( 378 unt; 0 typ; 0 def)
% Number of atoms : 1917 ( 520 equ; 0 cnn)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 12385 ( 822 ~; 565 |; 0 &;10998 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 9 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 13 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 2160 ( 0 ^;2160 !; 0 ?;2160 :)
% Comments :
%------------------------------------------------------------------------------
thf(theorem_decl,type,
theorem: $i > $o ).
thf(equivalent_decl,type,
equivalent: $i > $i > $i ).
thf(and_decl,type,
and: $i > $i > $i ).
thf(p_decl,type,
p: $i ).
thf(implies_decl,type,
implies: $i > $i > $i ).
thf(q_decl,type,
q: $i ).
thf(r_decl,type,
r: $i ).
thf(not_decl,type,
not: $i > $i ).
thf(axiom_decl,type,
axiom: $i > $o ).
thf(or_decl,type,
or: $i > $i > $i ).
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(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(175,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ and ) )
= ( B @ not @ ( A @ implies ) @ not ) ),
inference(rewrite,[status(thm)],[26,20]) ).
thf(196,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( D @ not ) )
| ( ( B @ ( A @ and ) @ ( C @ implies ) @ not )
= ( D @ ( C @ and ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,175]) ).
thf(197,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ and ) @ ( A @ implies ) @ not )
= ( C @ not @ ( B @ implies ) @ ( A @ and ) ) ),
inference(pattern_uni,[status(thm)],[196:[bind(A,$thf( E )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( G @ not @ ( E @ implies ) ))]]) ).
thf(220,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ and ) @ ( A @ implies ) @ not )
= ( C @ not @ ( B @ implies ) @ ( A @ and ) ) ),
inference(simp,[status(thm)],[197]) ).
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] :
( ( A @ ( B @ implies ) @ ( B @ ( A @ implies ) @ and ) )
= ( B @ ( A @ equivalent ) ) ),
inference(lifteq,[status(thm)],[27]) ).
thf(499,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ implies ) @ ( B @ ( A @ implies ) @ and ) )
!= ( D @ ( C @ and ) ) )
| ( ( B @ ( A @ equivalent ) )
= ( D @ not @ ( C @ implies ) @ not ) ) ),
inference(paramod_ordered,[status(thm)],[28,175]) ).
thf(500,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ equivalent ) )
= ( B @ ( A @ implies ) @ not @ ( A @ ( B @ implies ) @ implies ) @ not ) ),
inference(pattern_uni,[status(thm)],[499:[bind(A,$thf( H )),bind(B,$thf( G )),bind(C,$thf( G @ ( H @ implies ) )),bind(D,$thf( H @ ( G @ implies ) ))]]) ).
thf(539,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ equivalent ) )
= ( B @ ( A @ implies ) @ not @ ( A @ ( B @ implies ) @ implies ) @ not ) ),
inference(simp,[status(thm)],[500]) ).
thf(1,negated_conjecture,
~ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
thf(12,plain,
~ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(13,plain,
~ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ),
inference(polarity_switch,[status(thm)],[12]) ).
thf(190,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) ) )
| ~ ( B @ not @ ( A @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,13]) ).
thf(191,plain,
~ ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ),
inference(pattern_uni,[status(thm)],[190:[bind(A,$thf( p )),bind(B,$thf( q @ not @ ( r @ not @ implies ) ))]]) ).
thf(242,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( q @ not @ ( r @ not @ implies ) @ not ) )
| ~ ( B @ ( A @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,191]) ).
thf(243,plain,
~ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ),
inference(pattern_uni,[status(thm)],[242:[bind(A,$thf( r @ not )),bind(B,$thf( q ))]]) ).
thf(1311,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ equivalent ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( B @ ( A @ implies ) @ not @ ( A @ ( B @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[539,243]) ).
thf(1312,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1311:[bind(A,$thf( q @ ( r @ not @ and ) @ ( p @ implies ) @ not )),bind(B,$thf( r @ ( q @ implies ) @ ( p @ and ) ))]]) ).
thf(1499,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ and ) @ ( A @ implies ) @ not )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( C @ not @ ( B @ implies ) @ ( A @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[220,1312]) ).
thf(1500,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1499:[bind(A,$thf( p )),bind(B,$thf( r @ not )),bind(C,$thf( q ))]]) ).
thf(2198,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( B @ not @ ( A @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1500]) ).
thf(2199,plain,
~ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[2198:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
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(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(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(154,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(155,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[154:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( E @ not ))]]) ).
thf(173,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[155]) ).
thf(389,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ not @ ( C @ or ) ) )
| ( B @ ( A @ implies ) @ ( C @ ( D @ implies ) @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,173]) ).
thf(390,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ implies ) @ ( A @ not @ ( B @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[389:[bind(A,$thf( E )),bind(B,$thf( F @ not )),bind(C,$thf( E @ not )),bind(D,$thf( F ))]]) ).
thf(422,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ implies ) @ ( A @ not @ ( B @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[390]) ).
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(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(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(1626,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ ( A @ not @ ( B @ implies ) @ implies ) @ theorem )
!= ( C @ ( D @ ( D @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[422,66]) ).
thf(1627,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ ( A @ not @ ( B @ implies ) @ implies ) @ theorem )
!= ( C @ ( D @ ( D @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[1626]) ).
thf(1628,plain,
! [A: $i] : ( A @ not @ ( A @ not @ or ) @ not @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1627:[bind(A,$thf( N )),bind(B,$thf( N @ not @ ( N @ not @ or ) )),bind(C,$thf( N @ not @ ( N @ not @ or ) @ not @ ( N @ implies ) )),bind(D,$thf( N @ not ))]]) ).
thf(1642,plain,
! [A: $i] : ( A @ not @ ( A @ not @ or ) @ not @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[1628]) ).
thf(1706,plain,
! [A: $i] : ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem ),
inference(rewrite,[status(thm)],[1642,20]) ).
thf(1742,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ not @ ( A @ ( B @ implies ) @ implies ) @ not )
!= ( C @ not @ ( C @ implies ) @ not ) )
| ( A @ ( B @ equivalent ) @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[539,1706]) ).
thf(1743,plain,
! [A: $i] : ( A @ ( A @ equivalent ) @ ( A @ ( A @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1742:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ ( E @ implies ) ))]]) ).
thf(1763,plain,
! [A: $i] : ( A @ ( A @ equivalent ) @ ( A @ ( A @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[1743]) ).
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(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(4093,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ equivalent ) @ ( A @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1763,107]) ).
thf(4094,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ equivalent ) @ ( A @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4093]) ).
thf(4095,plain,
! [B: $i,A: $i] : ( B @ ( B @ equivalent ) @ ( B @ ( B @ implies ) @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4094:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ ( I @ equivalent ) @ ( I @ ( I @ implies ) @ implies ) ))]]) ).
thf(4188,plain,
! [B: $i,A: $i] : ( B @ ( B @ equivalent ) @ ( B @ ( B @ implies ) @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4095]) ).
thf(2205,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not ) )
| ~ ( B @ ( A @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1500]) ).
thf(2206,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[2205:[bind(A,$thf( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) )),bind(B,$thf( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) ))]]) ).
thf(2305,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ ( B @ not @ ( A @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,2206]) ).
thf(2306,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[2305:[bind(A,$thf( p )),bind(B,$thf( q @ not @ ( r @ not @ implies ) ))]]) ).
thf(163,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ~ ( C @ ( D @ implies ) @ theorem )
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[77,24]) ).
thf(164,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ ( C @ ( D @ implies ) @ theorem )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[163]) ).
thf(165,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[164:[bind(A,$thf( I )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( I @ or ) @ ( I @ ( J @ or ) @ implies ) ))]]) ).
thf(171,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( A @ ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[165]) ).
thf(13232,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem )
!= ( C @ ( E @ ( D @ or ) @ ( D @ ( E @ or ) @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[173,171]) ).
thf(13233,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ theorem )
!= ( C @ ( E @ ( D @ or ) @ ( D @ ( E @ or ) @ implies ) @ implies ) @ theorem ) )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[13232]) ).
thf(13234,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ not @ ( A @ ( B @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[13233:[bind(A,$thf( O @ ( P @ or ) )),bind(B,$thf( P @ ( O @ or ) )),bind(C,$thf( P @ ( O @ or ) @ not @ ( O @ ( P @ or ) @ or ) )),bind(D,$thf( P )),bind(E,$thf( O ))]]) ).
thf(13377,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ not @ ( A @ ( B @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[13234]) ).
thf(14466,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( B @ ( A @ implies ) @ not @ ( C @ ( D @ or ) @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,13377]) ).
thf(14467,plain,
! [B: $i,A: $i] : ( A @ ( B @ implies ) @ not @ ( B @ not @ ( A @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[14466:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(14603,plain,
! [B: $i,A: $i] : ( A @ ( B @ implies ) @ not @ ( B @ not @ ( A @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[14467]) ).
thf(160,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( C @ ( D @ implies ) @ theorem ) )
| ~ ( D @ theorem )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[77,24]) ).
thf(161,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( C @ ( D @ implies ) @ theorem ) )
| ~ ( D @ theorem )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[160]) ).
thf(162,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ or ) @ theorem )
| ( B @ ( A @ or ) @ theorem ) ),
inference(pattern_uni,[status(thm)],[161:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ or ) )),bind(D,$thf( G @ ( H @ or ) ))]]) ).
thf(170,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ or ) @ theorem )
| ( B @ ( A @ or ) @ theorem ) ),
inference(simp,[status(thm)],[162]) ).
thf(15839,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ implies ) @ not @ ( B @ not @ ( A @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[14603,170]) ).
thf(15840,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ implies ) @ not @ ( B @ not @ ( A @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[15839]) ).
thf(15841,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ or ) @ ( B @ ( A @ implies ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[15840:[bind(A,$thf( J )),bind(B,$thf( I )),bind(C,$thf( J @ ( I @ implies ) @ not )),bind(D,$thf( I @ not @ ( J @ or ) ))]]) ).
thf(16015,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ or ) @ ( B @ ( A @ implies ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[15841]) ).
thf(16808,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ or ) @ ( B @ ( A @ implies ) @ implies ) @ theorem ),
inference(rewrite,[status(thm)],[16015,20]) ).
thf(1613,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)],[173,66]) ).
thf(1614,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)],[1613]) ).
thf(1615,plain,
! [A: $i] : ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1614:[bind(A,$thf( K )),bind(B,$thf( K @ ( K @ or ) )),bind(C,$thf( K @ ( K @ or ) @ not @ ( K @ or ) )),bind(D,$thf( K ))]]) ).
thf(1639,plain,
! [A: $i] : ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1615]) ).
thf(1671,plain,
! [A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1639,13]) ).
thf(1672,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[1671]) ).
thf(1686,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[1672]) ).
thf(4072,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(4073,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)],[4072]) ).
thf(4074,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4073:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ or ) @ ( H @ implies ) ))]]) ).
thf(4183,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4074]) ).
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(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(261,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ not @ equivalent ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,243]) ).
thf(262,plain,
~ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ),
inference(pattern_uni,[status(thm)],[261:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(328,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,262]) ).
thf(329,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[328]) ).
thf(333,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) ) ),
inference(simp,[status(thm)],[329]) ).
thf(195,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( q @ not ) )
| ~ ( B @ ( A @ and ) @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,13]) ).
thf(217,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) )
!= q )
| ~ ( B @ ( A @ and ) @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[195]) ).
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(3091,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(3092,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)],[3091]) ).
thf(3093,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[3092:[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(3129,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[3093]) ).
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(3266,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)],[3129,90]) ).
thf(3267,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)],[3266]) ).
thf(3268,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[3267:[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(3285,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[3268]) ).
thf(2473,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[90,13]) ).
thf(2474,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2473]) ).
thf(2527,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2474]) ).
thf(4041,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(4042,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)],[4041]) ).
thf(4043,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4042:[bind(A,$thf( I )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( I @ or ) @ ( I @ ( J @ or ) @ implies ) ))]]) ).
thf(4176,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4043]) ).
thf(12362,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4176,170]) ).
thf(12363,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12362]) ).
thf(12364,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12363:[bind(A,$thf( A )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( K @ ( J @ or ) @ ( J @ ( K @ or ) @ implies ) )),bind(E,$thf( A ))]]) ).
thf(12539,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12364]) ).
thf(1620,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(1621,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)],[1620]) ).
thf(1622,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[1621:[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(1640,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[1622]) ).
thf(12208,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1640,170]) ).
thf(12209,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12208]) ).
thf(12210,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ ( B @ or ) @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12209:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( F @ ( F @ ( F @ or ) @ implies ) )),bind(D,$thf( A ))]]) ).
thf(12551,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ ( B @ or ) @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12210]) ).
thf(13501,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( B @ or ) @ implies ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[12551,90]) ).
thf(13502,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( B @ or ) @ implies ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[13501]) ).
thf(13503,plain,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( C @ ( C @ or ) @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[13502:[bind(A,$thf( F )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( F @ ( H @ ( H @ ( H @ or ) @ implies ) @ or ) ))]]) ).
thf(13548,plain,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( C @ ( C @ or ) @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[13503]) ).
thf(14464,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( D @ or ) ) )
| ( D @ ( C @ or ) @ not @ ( B @ ( A @ implies ) @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,13377]) ).
thf(14465,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ not @ ( A @ ( B @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[14464:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( E @ not ))]]) ).
thf(14602,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ not @ ( A @ ( B @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[14465]) ).
thf(1501,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ and ) @ ( A @ implies ) @ not )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( C @ not @ ( B @ implies ) @ ( A @ and ) @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[220,1312]) ).
thf(1502,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1501:[bind(A,$thf( p )),bind(B,$thf( r @ not )),bind(C,$thf( q ))]]) ).
thf(3480,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ not @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1502]) ).
thf(3481,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[3480:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(156,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(157,plain,
! [B: $i,A: $i] : ( A @ ( B @ implies ) @ ( B @ not @ ( A @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[156:[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)],[157]) ).
thf(15929,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( C @ ( D @ implies ) @ not ) )
| ( B @ ( A @ and ) @ ( D @ not @ ( C @ or ) @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,14603]) ).
thf(15930,plain,
! [B: $i,A: $i] : ( B @ ( A @ and ) @ ( A @ not @ ( B @ not @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[15929:[bind(A,$thf( A )),bind(B,$thf( E )),bind(C,$thf( E @ not )),bind(D,$thf( A ))]]) ).
thf(16008,plain,
! [B: $i,A: $i] : ( B @ ( A @ and ) @ ( A @ not @ ( B @ not @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[15930]) ).
thf(16024,plain,
! [B: $i,A: $i] : ( B @ ( A @ and ) @ ( A @ not @ ( B @ implies ) @ or ) @ theorem ),
inference(rewrite,[status(thm)],[16008,20]) ).
thf(16027,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ and ) @ ( A @ not @ ( B @ implies ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[16024,170]) ).
thf(16028,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ and ) @ ( A @ not @ ( B @ implies ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[16027]) ).
thf(16029,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ implies ) @ ( B @ ( A @ and ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[16028:[bind(A,$thf( H )),bind(B,$thf( I )),bind(C,$thf( I @ ( H @ and ) )),bind(D,$thf( H @ not @ ( I @ implies ) ))]]) ).
thf(16189,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ implies ) @ ( B @ ( A @ and ) @ or ) @ theorem ),
inference(simp,[status(thm)],[16029]) ).
thf(176,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( C @ not ) )
| ( ( D @ ( B @ ( A @ and ) @ or ) )
= ( D @ ( C @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,20]) ).
thf(177,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ and ) @ or ) )
= ( A @ ( C @ not @ ( B @ implies ) @ implies ) ) ),
inference(pattern_uni,[status(thm)],[176:[bind(A,$thf( E )),bind(B,$thf( G )),bind(C,$thf( G @ not @ ( E @ implies ) )),bind(D,$thf( D ))]]) ).
thf(225,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ and ) @ or ) )
= ( A @ ( C @ not @ ( B @ implies ) @ implies ) ) ),
inference(simp,[status(thm)],[177]) ).
thf(16491,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ implies ) @ ( B @ not @ ( A @ implies ) @ implies ) @ theorem ),
inference(rewrite,[status(thm)],[16189,225]) ).
thf(2491,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ equivalent ) @ ( A @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1763,90]) ).
thf(2492,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ equivalent ) @ ( A @ ( A @ implies ) @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2491]) ).
thf(2493,plain,
! [B: $i,A: $i] : ( B @ ( B @ equivalent ) @ ( B @ ( B @ implies ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2492:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ ( I @ equivalent ) @ ( I @ ( I @ implies ) @ implies ) ))]]) ).
thf(2548,plain,
! [B: $i,A: $i] : ( B @ ( B @ equivalent ) @ ( B @ ( B @ implies ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2493]) ).
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(2435,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)],[1639,90]) ).
thf(2436,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2435]) ).
thf(2437,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2436:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( H @ ( H @ or ) @ not @ ( H @ or ) ))]]) ).
thf(2531,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2437]) ).
thf(1337,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ equivalent ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( B @ ( A @ implies ) @ not @ ( A @ ( B @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[539,13]) ).
thf(1338,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1337:[bind(A,$thf( q @ not @ ( r @ not @ implies ) @ ( p @ and ) )),bind(B,$thf( r @ ( q @ implies ) @ ( p @ and ) ))]]) ).
thf(1834,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( B @ not @ ( A @ implies ) @ not @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1338]) ).
thf(1835,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1834:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(13293,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ equivalent ) @ ( A @ ( A @ implies ) @ implies ) @ theorem )
!= ( B @ ( D @ ( C @ or ) @ ( C @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ~ $true
| ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1763,171]) ).
thf(13294,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ equivalent ) @ ( A @ ( A @ implies ) @ implies ) @ theorem )
!= ( B @ ( D @ ( C @ or ) @ ( C @ ( D @ or ) @ implies ) @ implies ) @ theorem ) )
| ( B @ theorem ) ),
inference(simp,[status(thm)],[13293]) ).
thf(13295,plain,
! [A: $i] : ( A @ ( A @ or ) @ ( A @ ( A @ or ) @ equivalent ) @ theorem ),
inference(pattern_uni,[status(thm)],[13294:[bind(A,$thf( L @ ( L @ or ) )),bind(B,$thf( L @ ( L @ or ) @ ( L @ ( L @ or ) @ equivalent ) )),bind(C,$thf( L )),bind(D,$thf( L ))]]) ).
thf(13388,plain,
! [A: $i] : ( A @ ( A @ or ) @ ( A @ ( A @ or ) @ equivalent ) @ theorem ),
inference(simp,[status(thm)],[13295]) ).
thf(13744,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( C @ or ) ) )
| ( C @ ( C @ or ) @ ( B @ ( A @ implies ) @ equivalent ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,13388]) ).
thf(13745,plain,
! [A: $i] : ( A @ not @ ( A @ not @ or ) @ ( A @ not @ ( A @ implies ) @ equivalent ) @ theorem ),
inference(pattern_uni,[status(thm)],[13744:[bind(A,$thf( E )),bind(B,$thf( E @ not )),bind(C,$thf( E @ not ))]]) ).
thf(13881,plain,
! [A: $i] : ( A @ not @ ( A @ not @ or ) @ ( A @ not @ ( A @ implies ) @ equivalent ) @ theorem ),
inference(simp,[status(thm)],[13745]) ).
thf(16994,plain,
! [A: $i] : ( A @ not @ ( A @ implies ) @ ( A @ not @ ( A @ implies ) @ equivalent ) @ theorem ),
inference(rewrite,[status(thm)],[13881,20]) ).
thf(4105,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)],[1706,107]) ).
thf(4106,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)],[4105]) ).
thf(4107,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4106:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ not @ ( I @ implies ) @ not @ ( I @ implies ) ))]]) ).
thf(4156,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4107]) ).
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(5193,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)],[173,108]) ).
thf(5194,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)],[5193]) ).
thf(5195,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[5194:[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(5269,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[5195]) ).
thf(12391,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[3129,170]) ).
thf(12392,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12391]) ).
thf(12393,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( B @ implies ) @ ( C @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12392:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( I )),bind(D,$thf( I @ ( H @ implies ) @ ( I @ implies ) )),bind(E,$thf( A ))]]) ).
thf(12542,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( B @ implies ) @ ( C @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12393]) ).
thf(12660,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ implies ) @ ( C @ implies ) @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[12542,107]) ).
thf(12661,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ implies ) @ ( C @ implies ) @ or ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12660]) ).
thf(12662,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ implies ) @ ( D @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12661:[bind(A,$thf( G )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( G @ ( K @ ( J @ implies ) @ ( K @ implies ) @ or ) ))]]) ).
thf(12718,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ implies ) @ ( D @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[12662]) ).
thf(1852,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ and ) @ ( A @ implies ) @ not )
!= ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not ) )
| ~ ( C @ not @ ( B @ implies ) @ ( A @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[220,1338]) ).
thf(1853,plain,
~ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1852:[bind(A,$thf( q @ not @ ( r @ not @ implies ) @ ( p @ and ) )),bind(B,$thf( p )),bind(C,$thf( r @ ( q @ implies ) ))]]) ).
thf(4653,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ and ) @ ( A @ implies ) @ not )
!= ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not ) )
| ~ ( C @ not @ ( B @ implies ) @ ( A @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[220,1853]) ).
thf(4654,plain,
~ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[4653:[bind(A,$thf( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) )),bind(B,$thf( q @ not @ ( r @ not @ implies ) @ ( p @ and ) )),bind(C,$thf( r @ ( q @ implies ) @ not @ ( p @ implies ) ))]]) ).
thf(3486,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not ) )
| ~ ( B @ ( A @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1502]) ).
thf(3487,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[3486:[bind(A,$thf( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) )),bind(B,$thf( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) ))]]) ).
thf(3616,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( B @ not @ ( A @ implies ) @ not @ implies ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,3487]) ).
thf(3617,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[3616:[bind(A,$thf( p )),bind(B,$thf( q @ not @ ( r @ not @ implies ) ))]]) ).
thf(2488,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(2489,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)],[2488]) ).
thf(2490,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2489:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ implies ) @ ( H @ implies ) ))]]) ).
thf(2546,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( C @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2490]) ).
thf(4056,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)],[2546,107]) ).
thf(4057,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)],[4056]) ).
thf(4058,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4057:[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(4179,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4058]) ).
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(210,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( C @ not ) )
| ( B @ ( A @ and ) @ ( C @ not @ ( C @ implies ) @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,64]) ).
thf(211,plain,
! [B: $i,A: $i] : ( B @ ( A @ and ) @ ( B @ not @ ( A @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[210:[bind(A,$thf( D )),bind(B,$thf( F )),bind(C,$thf( F @ not @ ( D @ implies ) ))]]) ).
thf(228,plain,
! [B: $i,A: $i] : ( B @ ( A @ and ) @ ( B @ not @ ( A @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[211]) ).
thf(1623,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(1624,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)],[1623]) ).
thf(1625,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1624:[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(1641,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( B @ or ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[1625]) ).
thf(1717,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( C @ not @ ( C @ implies ) @ not ) )
| ( B @ ( A @ and ) @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1706]) ).
thf(1718,plain,
! [A: $i] : ( A @ ( A @ and ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1717:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(1768,plain,
! [A: $i] : ( A @ ( A @ and ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[1718]) ).
thf(1788,plain,
! [A: $i] :
( ( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1768,243]) ).
thf(1789,plain,
! [A: $i] :
( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[1788]) ).
thf(1815,plain,
! [A: $i] :
( ( A @ ( A @ and ) @ ( A @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[1789]) ).
thf(4049,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[107,13]) ).
thf(4050,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[4049]) ).
thf(4144,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[4050]) ).
thf(4910,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( B @ ( A @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,4144]) ).
thf(4911,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[4910:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(5020,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( A @ theorem ) ),
inference(simp,[status(thm)],[4911]) ).
thf(95,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,13]) ).
thf(96,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[95]) ).
thf(106,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[96]) ).
thf(183,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( q @ not ) )
| ( ( B @ ( A @ and ) @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( D @ ( C @ or ) @ ( D @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,106]) ).
thf(216,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) )
!= q )
| ( ( B @ ( A @ and ) @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( D @ ( C @ or ) @ ( D @ implies ) ) ) ),
inference(simp,[status(thm)],[183]) ).
thf(4027,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[107,243]) ).
thf(4028,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[4027]) ).
thf(4148,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[4028]) ).
thf(5044,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( B @ ( A @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( D @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,4148]) ).
thf(5045,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[5044:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(5158,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( A @ theorem ) ),
inference(simp,[status(thm)],[5045]) ).
thf(5905,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ( ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ not @ equivalent ) )
!= ( C @ ( D @ implies ) ) )
| ~ ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,5158]) ).
thf(5906,plain,
! [B: $i,A: $i] :
( ( ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) )
!= ( A @ ( B @ implies ) ) )
| ~ ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[5905:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(5957,plain,
! [B: $i,A: $i] :
( ( ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) )
!= ( A @ ( B @ implies ) ) )
| ~ ( A @ theorem ) ),
inference(simp,[status(thm)],[5906]) ).
thf(2460,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1768,90]) ).
thf(2461,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2460]) ).
thf(2462,plain,
! [B: $i,A: $i] : ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2461:[bind(A,$thf( G )),bind(B,$thf( B )),bind(C,$thf( G @ ( G @ and ) @ ( G @ implies ) ))]]) ).
thf(2540,plain,
! [B: $i,A: $i] : ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2462]) ).
thf(4024,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2540,107]) ).
thf(4025,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4024]) ).
thf(4026,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4025:[bind(A,$thf( E )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( J @ and ) @ ( J @ implies ) @ ( E @ implies ) ))]]) ).
thf(4173,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4026]) ).
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(371,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(372,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)],[371]) ).
thf(373,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ implies ) @ ( C @ ( A @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[372:[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(376,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ ( B @ or ) @ implies ) @ ( C @ ( A @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[373]) ).
thf(3620,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( B @ not @ ( A @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,3487]) ).
thf(3621,plain,
~ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[3620:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(134,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( B @ ( A @ implies ) @ ( D @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,106]) ).
thf(135,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(pattern_uni,[status(thm)],[134:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(136,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[135]) ).
thf(198,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) ) )
| ( ( B @ not @ ( A @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( C @ ( D @ implies ) @ ( C @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,136]) ).
thf(199,plain,
! [B: $i,A: $i] :
( ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( A @ ( B @ implies ) @ ( A @ implies ) ) ),
inference(pattern_uni,[status(thm)],[198:[bind(A,$thf( p )),bind(B,$thf( q @ not @ ( r @ not @ implies ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(221,plain,
! [B: $i,A: $i] :
( ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( A @ ( B @ implies ) @ ( A @ implies ) ) ),
inference(simp,[status(thm)],[199]) ).
thf(121,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(122,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)],[121]) ).
thf(123,plain,
! [A: $i] :
( ~ ( A @ not @ ( A @ implies ) @ theorem )
| ( A @ not @ theorem ) ),
inference(pattern_uni,[status(thm)],[122:[bind(A,$thf( G )),bind(B,$thf( G @ not )),bind(C,$thf( G @ not @ ( G @ implies ) ))]]) ).
thf(132,plain,
! [A: $i] :
( ~ ( A @ not @ ( A @ implies ) @ theorem )
| ( A @ not @ theorem ) ),
inference(simp,[status(thm)],[123]) ).
thf(68,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(69,plain,
! [B: $i,A: $i] : ( A @ ( B @ implies ) @ ( B @ not @ ( A @ or ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[68:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( E @ not ))]]) ).
thf(75,plain,
! [B: $i,A: $i] : ( A @ ( B @ implies ) @ ( B @ not @ ( A @ or ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[69]) ).
thf(305,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ not @ ( C @ or ) ) )
| ( C @ ( D @ implies ) @ ( B @ ( A @ implies ) @ implies ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[20,75]) ).
thf(306,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ implies ) @ ( B @ not @ ( A @ implies ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[305:[bind(A,$thf( E )),bind(B,$thf( F @ not )),bind(C,$thf( E @ not )),bind(D,$thf( F ))]]) ).
thf(312,plain,
! [B: $i,A: $i] : ( A @ not @ ( B @ implies ) @ ( B @ not @ ( A @ implies ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[306]) ).
thf(78,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,13]) ).
thf(79,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[78]) ).
thf(89,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(124,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(125,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)],[124]) ).
thf(126,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[125:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ not @ ( I @ not @ ( I @ implies ) @ implies ) ))]]) ).
thf(133,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ implies ) @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[126]) ).
thf(13494,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( B @ or ) @ implies ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[12551,107]) ).
thf(13495,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( B @ or ) @ implies ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[13494]) ).
thf(13496,plain,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( C @ ( C @ or ) @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[13495:[bind(A,$thf( F )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( F @ ( H @ ( H @ ( H @ or ) @ implies ) @ or ) ))]]) ).
thf(13547,plain,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( C @ ( C @ or ) @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[13496]) ).
thf(23136,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( C @ ( C @ or ) @ implies ) @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[13547,170]) ).
thf(23137,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( C @ ( C @ or ) @ implies ) @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[23136]) ).
thf(23138,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( B @ ( C @ ( C @ ( C @ or ) @ implies ) @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[23137:[bind(A,$thf( A )),bind(B,$thf( G )),bind(C,$thf( I )),bind(D,$thf( G @ ( I @ ( I @ ( I @ or ) @ implies ) @ or ) )),bind(E,$thf( A ))]]) ).
thf(23332,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( B @ ( C @ ( C @ ( C @ or ) @ implies ) @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[23138]) ).
thf(5180,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)],[376,108]) ).
thf(5181,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)],[5180]) ).
thf(5182,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[5181:[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(5281,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[5182]) ).
thf(12253,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ ( F @ or ) @ theorem ) )
| ~ $true
| ( F @ ( E @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4179,170]) ).
thf(12254,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ ( F @ or ) @ theorem ) )
| ( F @ ( E @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12253]) ).
thf(12255,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12254:[bind(A,$thf( A )),bind(B,$thf( G )),bind(C,$thf( K )),bind(D,$thf( L )),bind(E,$thf( L @ ( K @ implies ) @ ( L @ implies ) @ ( G @ implies ) )),bind(F,$thf( A ))]]) ).
thf(12561,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12255]) ).
thf(13828,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ ( A @ ( A @ or ) @ equivalent ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[13388,107]) ).
thf(13829,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ ( A @ ( A @ or ) @ equivalent ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[13828]) ).
thf(13830,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ ( B @ ( B @ or ) @ equivalent ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[13829:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ ( I @ or ) @ ( I @ ( I @ or ) @ equivalent ) ))]]) ).
thf(13876,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ ( B @ ( B @ or ) @ equivalent ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[13830]) ).
thf(24003,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ or ) @ ( B @ ( B @ or ) @ equivalent ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[13876,170]) ).
thf(24004,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ or ) @ ( B @ ( B @ or ) @ equivalent ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[24003]) ).
thf(24005,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ or ) @ ( B @ ( B @ or ) @ equivalent ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[24004:[bind(A,$thf( A )),bind(B,$thf( J )),bind(C,$thf( J @ ( J @ or ) @ ( J @ ( J @ or ) @ equivalent ) )),bind(D,$thf( A ))]]) ).
thf(24197,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ or ) @ ( B @ ( B @ or ) @ equivalent ) @ or ) @ theorem ),
inference(simp,[status(thm)],[24005]) ).
thf(2465,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(2466,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)],[2465]) ).
thf(2467,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2466:[bind(A,$thf( I )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( I @ or ) @ ( I @ ( J @ or ) @ implies ) ))]]) ).
thf(2541,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2467]) ).
thf(1518,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ ( r @ not @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( B @ not @ ( A @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1312]) ).
thf(1519,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1518:[bind(A,$thf( r @ not )),bind(B,$thf( q ))]]) ).
thf(4031,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[1768,107]) ).
thf(4032,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4031]) ).
thf(4033,plain,
! [B: $i,A: $i] : ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4032:[bind(A,$thf( G )),bind(B,$thf( B )),bind(C,$thf( G @ ( G @ and ) @ ( G @ implies ) ))]]) ).
thf(4174,plain,
! [B: $i,A: $i] : ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4033]) ).
thf(12456,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4174,170]) ).
thf(12457,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12456]) ).
thf(12458,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ and ) @ ( B @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12457:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( H @ ( H @ and ) @ ( H @ implies ) )),bind(D,$thf( A ))]]) ).
thf(12550,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ and ) @ ( B @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12458]) ).
thf(1503,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ and ) @ ( A @ implies ) @ not )
!= ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not ) )
| ~ ( C @ not @ ( B @ implies ) @ ( A @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[220,1312]) ).
thf(1504,plain,
~ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1503:[bind(A,$thf( q @ ( r @ not @ and ) @ ( p @ implies ) @ not )),bind(B,$thf( p )),bind(C,$thf( r @ ( q @ implies ) ))]]) ).
thf(4498,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ and ) @ ( A @ implies ) @ not )
!= ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not ) )
| ~ ( C @ not @ ( B @ implies ) @ ( A @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[220,1504]) ).
thf(4499,plain,
~ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[4498:[bind(A,$thf( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) )),bind(B,$thf( q @ ( r @ not @ and ) @ ( p @ implies ) @ not )),bind(C,$thf( r @ ( q @ implies ) @ not @ ( p @ implies ) ))]]) ).
thf(259,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,243]) ).
thf(260,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[259]) ).
thf(275,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[260]) ).
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(180,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ( ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( B @ not @ ( A @ implies ) @ not @ equivalent ) )
!= ( D @ ( C @ or ) @ ( D @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,106]) ).
thf(181,plain,
! [B: $i,A: $i] :
( ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) )
!= ( B @ ( A @ or ) @ ( B @ implies ) ) ),
inference(pattern_uni,[status(thm)],[180:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(229,plain,
! [B: $i,A: $i] :
( ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) )
!= ( B @ ( A @ or ) @ ( B @ implies ) ) ),
inference(simp,[status(thm)],[181]) ).
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(5311,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5269,13]) ).
thf(5312,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[5311]) ).
thf(5382,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ or ) @ or ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[5312]) ).
thf(6692,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( D @ not @ ( B @ ( A @ implies ) @ or ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,5382]) ).
thf(6693,plain,
! [B: $i,A: $i] :
( ( A @ not @ ( A @ ( B @ implies ) @ or ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(pattern_uni,[status(thm)],[6692:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(6708,plain,
! [B: $i,A: $i] :
( ( A @ not @ ( A @ ( B @ implies ) @ or ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[6693]) ).
thf(1800,plain,
! [A: $i] :
( ( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1768,191]) ).
thf(1801,plain,
! [A: $i] :
( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[1800]) ).
thf(1819,plain,
! [A: $i] :
( ( A @ ( A @ and ) @ ( A @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[1801]) ).
thf(2485,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(2486,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)],[2485]) ).
thf(2487,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2486:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ or ) @ ( H @ implies ) ))]]) ).
thf(2545,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2487]) ).
thf(4090,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)],[2545,107]) ).
thf(4091,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)],[4090]) ).
thf(4092,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4091:[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(4187,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4092]) ).
thf(2427,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)],[1640,90]) ).
thf(2428,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)],[2427]) ).
thf(2429,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2428:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ ( H @ or ) @ implies ) @ ( E @ or ) ))]]) ).
thf(2547,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2429]) ).
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(206,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( C @ not ) )
| ( B @ ( A @ and ) @ ( C @ not @ ( C @ implies ) @ implies ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[175,34]) ).
thf(207,plain,
! [B: $i,A: $i] : ( B @ ( A @ and ) @ ( B @ not @ ( A @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ implies ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[206:[bind(A,$thf( D )),bind(B,$thf( F )),bind(C,$thf( F @ not @ ( D @ implies ) ))]]) ).
thf(224,plain,
! [B: $i,A: $i] : ( B @ ( A @ and ) @ ( B @ not @ ( A @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ implies ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[207]) ).
thf(232,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[77,191]) ).
thf(233,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[232]) ).
thf(252,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[233]) ).
thf(1836,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( B @ not @ ( A @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1338]) ).
thf(1837,plain,
~ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1836:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(13067,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ and ) @ ( B @ implies ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[12550,107]) ).
thf(13068,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ and ) @ ( B @ implies ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[13067]) ).
thf(13069,plain,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( C @ and ) @ ( C @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[13068:[bind(A,$thf( F )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( F @ ( J @ ( J @ and ) @ ( J @ implies ) @ or ) ))]]) ).
thf(13116,plain,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( C @ and ) @ ( C @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[13069]) ).
thf(4099,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)],[1639,107]) ).
thf(4100,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4099]) ).
thf(4101,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4100:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( H @ ( H @ or ) @ not @ ( H @ or ) ))]]) ).
thf(4154,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4101]) ).
thf(12359,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4154,170]) ).
thf(12360,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ or ) @ not @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12359]) ).
thf(12361,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ or ) @ not @ ( B @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12360:[bind(A,$thf( A )),bind(B,$thf( I )),bind(C,$thf( I @ ( I @ or ) @ not @ ( I @ or ) )),bind(D,$thf( A ))]]) ).
thf(12538,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ or ) @ not @ ( B @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12361]) ).
thf(3081,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)],[173,91]) ).
thf(3082,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)],[3081]) ).
thf(3083,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[3082:[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(3127,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[3083]) ).
thf(4096,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)],[3127,107]) ).
thf(4097,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)],[4096]) ).
thf(4098,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4097:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ implies ) @ or ) ))]]) ).
thf(4153,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4098]) ).
thf(12417,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4153,170]) ).
thf(12418,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12417]) ).
thf(12419,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ not @ ( C @ ( B @ implies ) @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12418:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( J )),bind(D,$thf( J @ not @ ( J @ ( H @ implies ) @ or ) )),bind(E,$thf( A ))]]) ).
thf(12546,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ not @ ( C @ ( B @ implies ) @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12419]) ).
thf(158,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[77,13]) ).
thf(159,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[158]) ).
thf(169,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[159]) ).
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(14445,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ not @ ( A @ ( B @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[13377,170]) ).
thf(14446,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ not @ ( A @ ( B @ or ) @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[14445]) ).
thf(14447,plain,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[14446:[bind(A,$thf( H )),bind(B,$thf( I )),bind(C,$thf( I @ ( H @ or ) @ not )),bind(D,$thf( H @ ( I @ or ) ))]]) ).
thf(14616,plain,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ not @ or ) @ theorem ),
inference(simp,[status(thm)],[14447]) ).
thf(14623,plain,
! [B: $i,A: $i] : ( A @ ( B @ or ) @ ( B @ ( A @ or ) @ implies ) @ theorem ),
inference(rewrite,[status(thm)],[14616,20]) ).
thf(315,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[49,262]) ).
thf(316,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[315]) ).
thf(339,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ or ) @ ( B @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) ) ),
inference(simp,[status(thm)],[316]) ).
thf(192,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( B @ not @ ( A @ implies ) @ not @ equivalent ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,13]) ).
thf(193,plain,
~ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ),
inference(pattern_uni,[status(thm)],[192:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(2307,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( B @ not @ ( A @ implies ) @ not @ implies ) @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,2206]) ).
thf(2308,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[2307:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(6538,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ and ) @ ( A @ implies ) @ not )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( C @ not @ ( B @ implies ) @ ( A @ and ) @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[220,2308]) ).
thf(6539,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[6538:[bind(A,$thf( p )),bind(B,$thf( r @ not )),bind(C,$thf( q ))]]) ).
thf(202,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( r @ not ) )
| ( ( q @ not @ ( B @ ( A @ and ) @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( C @ ( D @ implies ) @ ( C @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,136]) ).
thf(212,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) )
!= r )
| ( ( q @ not @ ( B @ ( A @ and ) @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( C @ ( D @ implies ) @ ( C @ implies ) ) ) ),
inference(simp,[status(thm)],[202]) ).
thf(2468,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[90,193]) ).
thf(2469,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2468]) ).
thf(2519,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2469]) ).
thf(1830,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1338]) ).
thf(1831,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1830:[bind(A,$thf( p )),bind(B,$thf( q @ not @ ( r @ not @ implies ) ))]]) ).
thf(4087,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)],[3129,107]) ).
thf(4088,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)],[4087]) ).
thf(4089,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4088:[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(4186,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4089]) ).
thf(12332,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( E @ ( F @ or ) @ theorem ) )
| ~ $true
| ( F @ ( E @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4186,170]) ).
thf(12333,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( E @ ( F @ or ) @ theorem ) )
| ( F @ ( E @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12332]) ).
thf(12334,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12333:[bind(A,$thf( A )),bind(B,$thf( G )),bind(C,$thf( K )),bind(D,$thf( L )),bind(E,$thf( L @ ( K @ implies ) @ ( L @ implies ) @ ( G @ or ) )),bind(F,$thf( A ))]]) ).
thf(12533,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12334]) ).
thf(4113,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[107,262]) ).
thf(4114,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[4113]) ).
thf(4152,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[4114]) ).
thf(1728,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1706,243]) ).
thf(1729,plain,
! [A: $i] :
( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[1728]) ).
thf(1759,plain,
! [A: $i] :
( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[1729]) ).
thf(3185,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)],[3127,90]) ).
thf(3186,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)],[3185]) ).
thf(3187,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[3186:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ implies ) @ or ) ))]]) ).
thf(3215,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[3187]) ).
thf(3999,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)],[1640,107]) ).
thf(4000,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)],[3999]) ).
thf(4001,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4000:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ ( H @ or ) @ implies ) @ ( E @ or ) ))]]) ).
thf(4163,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4001]) ).
thf(236,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ not @ equivalent ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,191]) ).
thf(237,plain,
~ ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ),
inference(pattern_uni,[status(thm)],[236:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(1796,plain,
! [A: $i] :
( ( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1768,193]) ).
thf(1797,plain,
! [A: $i] :
( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[1796]) ).
thf(1814,plain,
! [A: $i] :
( ( A @ ( A @ and ) @ ( A @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) ) ),
inference(simp,[status(thm)],[1797]) ).
thf(12216,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4183,170]) ).
thf(12217,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ or ) @ ( C @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12216]) ).
thf(12218,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( B @ or ) @ ( C @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12217:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( I )),bind(D,$thf( I @ ( H @ or ) @ ( I @ implies ) )),bind(E,$thf( A ))]]) ).
thf(12553,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( B @ or ) @ ( C @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12218]) ).
thf(1514,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( B @ not @ ( A @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1312]) ).
thf(1515,plain,
~ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1514:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(22049,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( C @ and ) @ ( C @ implies ) @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[13116,170]) ).
thf(22050,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ ( C @ and ) @ ( C @ implies ) @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[22049]) ).
thf(22051,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( B @ ( C @ ( C @ and ) @ ( C @ implies ) @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[22050:[bind(A,$thf( A )),bind(B,$thf( G )),bind(C,$thf( K )),bind(D,$thf( G @ ( K @ ( K @ and ) @ ( K @ implies ) @ or ) )),bind(E,$thf( A ))]]) ).
thf(22233,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( B @ ( C @ ( C @ and ) @ ( C @ implies ) @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[22051]) ).
thf(2494,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)],[1706,90]) ).
thf(2495,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)],[2494]) ).
thf(2496,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2495:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ not @ ( I @ implies ) @ not @ ( I @ implies ) ))]]) ).
thf(2529,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2496]) ).
thf(6545,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ not @ ( B @ implies ) @ ( A @ and ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ ( C @ ( B @ and ) @ ( A @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[220,2308]) ).
thf(6546,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[6545:[bind(A,$thf( p )),bind(B,$thf( r @ not )),bind(C,$thf( q ))]]) ).
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(267,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[64,243]) ).
thf(268,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[267]) ).
thf(279,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[268]) ).
thf(2503,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[90,262]) ).
thf(2504,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2503]) ).
thf(2524,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2504]) ).
thf(145,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(146,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)],[145]) ).
thf(147,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ ( B @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[146:[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(149,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ or ) @ ( A @ or ) @ ( C @ ( A @ or ) @ ( B @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[147]) ).
thf(1832,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( B @ not @ ( A @ implies ) @ not @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1338]) ).
thf(1833,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1832:[bind(A,$thf( p )),bind(B,$thf( q @ not @ ( r @ not @ implies ) ))]]) ).
thf(5356,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)],[5269,90]) ).
thf(5357,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)],[5356]) ).
thf(5358,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[5357:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ or ) @ or ) ))]]) ).
thf(5395,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[5358]) ).
thf(2481,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[90,191]) ).
thf(2482,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2481]) ).
thf(2525,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2482]) ).
thf(1734,plain,
! [A: $i] :
( ( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1706,13]) ).
thf(1735,plain,
! [A: $i] :
( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[1734]) ).
thf(1752,plain,
! [A: $i] :
( ( A @ not @ ( A @ implies ) @ not @ ( A @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[1735]) ).
thf(52,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47,13]) ).
thf(53,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[52]) ).
thf(63,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[53]) ).
thf(116,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( C @ ( C @ or ) ) )
| ( ( C @ ( B @ ( A @ implies ) @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,63]) ).
thf(117,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(pattern_uni,[status(thm)],[116:[bind(A,$thf( E )),bind(B,$thf( E @ not )),bind(C,$thf( E @ not ))]]) ).
thf(118,plain,
! [A: $i] :
( ( A @ not @ ( A @ not @ ( A @ implies ) @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[117]) ).
thf(5296,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[5269,243]) ).
thf(5297,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ or ) @ or ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[5296]) ).
thf(5367,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ or ) @ or ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[5297]) ).
thf(6474,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( D @ not @ ( B @ ( A @ implies ) @ or ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,5367]) ).
thf(6475,plain,
! [B: $i,A: $i] :
( ( A @ not @ ( A @ ( B @ implies ) @ or ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(pattern_uni,[status(thm)],[6474:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(6493,plain,
! [B: $i,A: $i] :
( ( A @ not @ ( A @ ( B @ implies ) @ or ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[6475]) ).
thf(21228,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( D @ ( C @ implies ) @ ( D @ implies ) @ or ) @ ( A @ or ) @ theorem )
!= ( E @ ( F @ or ) @ theorem ) )
| ~ $true
| ( F @ ( E @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[12718,170]) ).
thf(21229,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( D @ ( C @ implies ) @ ( D @ implies ) @ or ) @ ( A @ or ) @ theorem )
!= ( E @ ( F @ or ) @ theorem ) )
| ( F @ ( E @ or ) @ theorem ) ),
inference(simp,[status(thm)],[21228]) ).
thf(21230,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( B @ ( D @ ( C @ implies ) @ ( D @ implies ) @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[21229:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( L )),bind(E,$thf( H @ ( L @ ( K @ implies ) @ ( L @ implies ) @ or ) )),bind(F,$thf( A ))]]) ).
thf(21413,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( B @ ( D @ ( C @ implies ) @ ( D @ implies ) @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[21230]) ).
thf(4338,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)],[4183,107]) ).
thf(4339,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)],[4338]) ).
thf(4340,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4339:[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(4373,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4340]) ).
thf(12384,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( E @ ( F @ or ) @ theorem ) )
| ~ $true
| ( F @ ( E @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4373,170]) ).
thf(12385,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( E @ ( F @ or ) @ theorem ) )
| ( F @ ( E @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12384]) ).
thf(12386,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12385:[bind(A,$thf( A )),bind(B,$thf( G )),bind(C,$thf( K )),bind(D,$thf( L )),bind(E,$thf( L @ ( K @ or ) @ ( L @ implies ) @ ( G @ or ) )),bind(F,$thf( A ))]]) ).
thf(12541,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12386]) ).
thf(435,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ ( C @ or ) ) )
| ( ( B @ ( A @ implies ) @ ( D @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ) ),
inference(paramod_ordered,[status(thm)],[20,275]) ).
thf(436,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(pattern_uni,[status(thm)],[435:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(445,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ implies ) @ ( A @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[436]) ).
thf(3070,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)],[376,91]) ).
thf(3071,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)],[3070]) ).
thf(3072,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( A @ or ) @ ( C @ ( A @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[3071:[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(3123,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( B @ implies ) @ ( A @ or ) @ ( C @ ( A @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[3072]) ).
thf(3618,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ not @ implies ) @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,3487]) ).
thf(3619,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[3618:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(4044,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[107,193]) ).
thf(4045,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[4044]) ).
thf(4149,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[4045]) ).
thf(4018,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)],[1641,107]) ).
thf(4019,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)],[4018]) ).
thf(4020,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4019:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ ( H @ or ) @ implies ) @ ( E @ implies ) ))]]) ).
thf(4171,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4020]) ).
thf(4245,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4174,107]) ).
thf(4246,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[4245]) ).
thf(4247,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[4246:[bind(A,$thf( E )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( J @ and ) @ ( J @ implies ) @ ( E @ or ) ))]]) ).
thf(4273,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[4247]) ).
thf(2034,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,1640]) ).
thf(2035,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[2034:[bind(A,$thf( F )),bind(B,$thf( F @ not )),bind(C,$thf( C )),bind(D,$thf( F @ not ))]]) ).
thf(2079,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[2035]) ).
thf(166,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( ( C @ ( D @ implies ) )
!= D )
| ~ $true
| ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[77,37]) ).
thf(167,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ ( A @ ( B @ or ) @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( ( C @ ( D @ implies ) )
!= D )
| ( C @ theorem ) ),
inference(simp,[status(thm)],[166]) ).
thf(168,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ implies ) )
!= ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) ) )
| ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[167:[bind(A,$thf( I )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( I @ or ) @ ( I @ ( J @ or ) @ implies ) ))]]) ).
thf(172,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) @ implies ) )
!= ( C @ ( B @ or ) @ ( B @ ( C @ or ) @ implies ) ) )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[168]) ).
thf(182,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( r @ not ) )
| ( ( q @ not @ ( B @ ( A @ and ) @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( D @ ( C @ or ) @ ( D @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,106]) ).
thf(219,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) )
!= r )
| ( ( q @ not @ ( B @ ( A @ and ) @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( D @ ( C @ or ) @ ( D @ implies ) ) ) ),
inference(simp,[status(thm)],[182]) ).
thf(269,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[48,243]) ).
thf(270,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[269]) ).
thf(274,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ implies ) @ ( B @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[270]) ).
thf(184,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) ) )
| ( ( B @ not @ ( A @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( D @ ( C @ implies ) @ ( D @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,89]) ).
thf(185,plain,
! [B: $i,A: $i] :
( ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( B @ ( A @ implies ) @ ( B @ implies ) ) ),
inference(pattern_uni,[status(thm)],[184:[bind(A,$thf( p )),bind(B,$thf( q @ not @ ( r @ not @ implies ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(230,plain,
! [B: $i,A: $i] :
( ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( B @ ( A @ implies ) @ ( B @ implies ) ) ),
inference(simp,[status(thm)],[185]) ).
thf(70,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(71,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[70:[bind(A,$thf( E )),bind(B,$thf( B )),bind(C,$thf( E @ not )),bind(D,$thf( B ))]]) ).
thf(76,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ or ) @ ( A @ ( B @ implies ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[71]) ).
thf(12356,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2079,170]) ).
thf(12357,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12356]) ).
thf(12358,plain,
! [B: $i,A: $i] : ( A @ ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12357:[bind(A,$thf( A )),bind(B,$thf( J )),bind(C,$thf( J @ not @ ( J @ not @ ( J @ implies ) @ implies ) )),bind(D,$thf( A ))]]) ).
thf(12537,plain,
! [B: $i,A: $i] : ( A @ ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12358]) ).
thf(4343,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)],[4183,90]) ).
thf(4344,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)],[4343]) ).
thf(4345,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[4344:[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(4374,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[4345]) ).
thf(2196,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( B @ not @ ( A @ implies ) @ not @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1500]) ).
thf(2197,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[2196:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(2450,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)],[1641,90]) ).
thf(2451,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)],[2450]) ).
thf(2452,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2451:[bind(A,$thf( E )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( H @ ( H @ or ) @ implies ) @ ( E @ implies ) ))]]) ).
thf(2538,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2452]) ).
thf(2593,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[2540,90]) ).
thf(2594,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ implies ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[2593]) ).
thf(2595,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2594:[bind(A,$thf( E )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( J @ and ) @ ( J @ implies ) @ ( E @ implies ) ))]]) ).
thf(2610,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2595]) ).
thf(2313,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ ( r @ not @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( B @ not @ ( A @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,2206]) ).
thf(2314,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[2313:[bind(A,$thf( r @ not )),bind(B,$thf( q ))]]) ).
thf(189,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( q @ not ) )
| ( ( B @ ( A @ and ) @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( D @ ( C @ implies ) @ ( D @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,89]) ).
thf(213,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) )
!= q )
| ( ( B @ ( A @ and ) @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( D @ ( C @ implies ) @ ( D @ implies ) ) ) ),
inference(simp,[status(thm)],[189]) ).
thf(5351,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)],[5269,107]) ).
thf(5352,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)],[5351]) ).
thf(5353,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[5352:[bind(A,$thf( G )),bind(B,$thf( I )),bind(C,$thf( C )),bind(D,$thf( I @ not @ ( I @ ( G @ or ) @ or ) ))]]) ).
thf(5392,plain,
! [C: $i,B: $i,A: $i] : ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[5353]) ).
thf(12339,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4171,170]) ).
thf(12340,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12339]) ).
thf(12341,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12340:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( I )),bind(D,$thf( I @ ( I @ ( I @ or ) @ implies ) @ ( F @ implies ) )),bind(E,$thf( A ))]]) ).
thf(12534,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12341]) ).
thf(271,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47,243]) ).
thf(272,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[271]) ).
thf(278,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[272]) ).
thf(204,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( C @ not ) )
| ( C @ not @ ( B @ ( A @ and ) @ ( C @ implies ) @ implies ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[175,34]) ).
thf(205,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ implies ) @ not @ ( B @ ( A @ and ) @ ( B @ not @ ( A @ implies ) @ implies ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[204:[bind(A,$thf( D )),bind(B,$thf( F )),bind(C,$thf( F @ not @ ( D @ implies ) ))]]) ).
thf(223,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ implies ) @ not @ ( B @ ( A @ and ) @ ( B @ not @ ( A @ implies ) @ implies ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[205]) ).
thf(295,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47,193]) ).
thf(296,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[295]) ).
thf(299,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) ) ),
inference(simp,[status(thm)],[296]) ).
thf(208,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( C @ not ) )
| ( C @ not @ ( B @ ( A @ and ) @ ( C @ implies ) @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,64]) ).
thf(209,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ implies ) @ not @ ( B @ ( A @ and ) @ ( B @ not @ ( A @ implies ) @ implies ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[208:[bind(A,$thf( D )),bind(B,$thf( F )),bind(C,$thf( F @ not @ ( D @ implies ) ))]]) ).
thf(226,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ implies ) @ not @ ( B @ ( A @ and ) @ ( B @ not @ ( A @ implies ) @ implies ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[209]) ).
thf(1661,plain,
! [A: $i] :
( ( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1639,243]) ).
thf(1662,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[1661]) ).
thf(1694,plain,
! [A: $i] :
( ( A @ ( A @ or ) @ not @ ( A @ or ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[1662]) ).
thf(12241,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4156,170]) ).
thf(12242,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12241]) ).
thf(12243,plain,
! [B: $i,A: $i] : ( A @ ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12242:[bind(A,$thf( A )),bind(B,$thf( J )),bind(C,$thf( J @ not @ ( J @ implies ) @ not @ ( J @ implies ) )),bind(D,$thf( A ))]]) ).
thf(12557,plain,
! [B: $i,A: $i] : ( A @ ( B @ not @ ( B @ implies ) @ not @ ( B @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12243]) ).
thf(5734,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) ) )
| ( ( B @ not @ ( A @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( C @ ( D @ implies ) ) )
| ~ ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,5020]) ).
thf(5735,plain,
! [B: $i,A: $i] :
( ( ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( A @ ( B @ implies ) ) )
| ~ ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[5734:[bind(A,$thf( p )),bind(B,$thf( q @ not @ ( r @ not @ implies ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(5812,plain,
! [B: $i,A: $i] :
( ( ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( A @ ( B @ implies ) ) )
| ~ ( A @ theorem ) ),
inference(simp,[status(thm)],[5735]) ).
thf(3159,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3127,13]) ).
thf(3160,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[3159]) ).
thf(3206,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ implies ) @ or ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[3160]) ).
thf(13074,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ and ) @ ( B @ implies ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[12550,90]) ).
thf(13075,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ and ) @ ( B @ implies ) @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[13074]) ).
thf(13076,plain,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( C @ and ) @ ( C @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[13075:[bind(A,$thf( F )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( F @ ( J @ ( J @ and ) @ ( J @ implies ) @ or ) ))]]) ).
thf(13117,plain,
! [C: $i,B: $i,A: $i] : ( B @ ( C @ ( C @ and ) @ ( C @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[13076]) ).
thf(3506,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ and ) @ ( A @ implies ) @ not )
!= ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ not ) )
| ~ ( C @ not @ ( B @ implies ) @ ( A @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[220,1502]) ).
thf(3507,plain,
~ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[3506:[bind(A,$thf( q @ not @ ( r @ not @ implies ) @ ( p @ and ) )),bind(B,$thf( p )),bind(C,$thf( r @ ( q @ implies ) ))]]) ).
thf(141,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(142,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)],[141:[bind(A,$thf( F )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( F @ not )),bind(E,$thf( B ))]]) ).
thf(152,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( B @ or ) @ ( C @ not @ or ) @ ( A @ ( C @ implies ) @ ( B @ or ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[142]) ).
thf(11611,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( B @ or ) @ ( C @ implies ) @ ( A @ ( C @ implies ) @ ( B @ or ) @ implies ) @ axiom ),
inference(rewrite,[status(thm)],[152,20]) ).
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(1810,plain,
! [A: $i] :
( ( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1768,262]) ).
thf(1811,plain,
! [A: $i] :
( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[1810]) ).
thf(1813,plain,
! [A: $i] :
( ( A @ ( A @ and ) @ ( A @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) ) ),
inference(simp,[status(thm)],[1811]) ).
thf(1606,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)],[376,66]) ).
thf(1607,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)],[1606]) ).
thf(1608,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ ( A @ or ) @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[1607:[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(1637,plain,
! [B: $i,A: $i] : ( B @ ( A @ or ) @ ( B @ ( B @ or ) @ ( A @ or ) @ implies ) @ theorem ),
inference(simp,[status(thm)],[1608]) ).
thf(12667,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ implies ) @ ( C @ implies ) @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[12542,90]) ).
thf(12668,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ implies ) @ ( C @ implies ) @ or ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[12667]) ).
thf(12669,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ implies ) @ ( D @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[12668:[bind(A,$thf( G )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( G @ ( K @ ( J @ implies ) @ ( K @ implies ) @ or ) ))]]) ).
thf(12720,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ implies ) @ ( D @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[12669]) ).
thf(12379,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[5392,170]) ).
thf(12380,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ not @ ( C @ ( B @ or ) @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12379]) ).
thf(12381,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ not @ ( C @ ( B @ or ) @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12380:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( J )),bind(D,$thf( J @ not @ ( J @ ( H @ or ) @ or ) )),bind(E,$thf( A ))]]) ).
thf(12540,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ not @ ( C @ ( B @ or ) @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12381]) ).
thf(15674,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( D @ not @ ( C @ or ) ) )
| ( B @ ( A @ implies ) @ not @ ( C @ ( D @ implies ) @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[20,14602]) ).
thf(15675,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ implies ) @ not @ ( A @ not @ ( B @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[15674:[bind(A,$thf( E )),bind(B,$thf( F @ not )),bind(C,$thf( E @ not )),bind(D,$thf( F ))]]) ).
thf(15828,plain,
! [B: $i,A: $i] : ( B @ not @ ( A @ implies ) @ not @ ( A @ not @ ( B @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[15675]) ).
thf(330,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47,262]) ).
thf(331,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[330]) ).
thf(336,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) ) ),
inference(simp,[status(thm)],[331]) ).
thf(13660,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ or ) @ ( C @ implies ) @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[12553,107]) ).
thf(13661,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ or ) @ ( C @ implies ) @ or ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[13660]) ).
thf(13662,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ or ) @ ( D @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[13661:[bind(A,$thf( G )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( G @ ( K @ ( J @ or ) @ ( K @ implies ) @ or ) ))]]) ).
thf(13720,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ or ) @ ( D @ implies ) @ or ) @ ( A @ or ) @ theorem ),
inference(simp,[status(thm)],[13662]) ).
thf(23588,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( D @ ( C @ or ) @ ( D @ implies ) @ or ) @ ( A @ or ) @ theorem )
!= ( E @ ( F @ or ) @ theorem ) )
| ~ $true
| ( F @ ( E @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[13720,170]) ).
thf(23589,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( D @ ( C @ or ) @ ( D @ implies ) @ or ) @ ( A @ or ) @ theorem )
!= ( E @ ( F @ or ) @ theorem ) )
| ( F @ ( E @ or ) @ theorem ) ),
inference(simp,[status(thm)],[23588]) ).
thf(23590,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( B @ ( D @ ( C @ or ) @ ( D @ implies ) @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[23589:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( L )),bind(E,$thf( H @ ( L @ ( K @ or ) @ ( L @ implies ) @ or ) )),bind(F,$thf( A ))]]) ).
thf(23774,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( B @ ( D @ ( C @ or ) @ ( D @ implies ) @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[23590]) ).
thf(1798,plain,
! [A: $i] :
( ( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1768,13]) ).
thf(1799,plain,
! [A: $i] :
( ( A @ ( A @ and ) @ ( A @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[1798]) ).
thf(1817,plain,
! [A: $i] :
( ( A @ ( A @ and ) @ ( A @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[1799]) ).
thf(2309,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( B @ not @ ( A @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,2206]) ).
thf(2310,plain,
~ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[2309:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(487,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ( ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ not @ equivalent ) )
!= ( C @ ( D @ implies ) @ ( C @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,445]) ).
thf(488,plain,
! [B: $i,A: $i] :
( ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) )
!= ( A @ ( B @ implies ) @ ( A @ implies ) ) ),
inference(pattern_uni,[status(thm)],[487:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(495,plain,
! [B: $i,A: $i] :
( ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) )
!= ( A @ ( B @ implies ) @ ( A @ implies ) ) ),
inference(simp,[status(thm)],[488]) ).
thf(1516,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ ( r @ not @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1312]) ).
thf(1517,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1516:[bind(A,$thf( r @ not )),bind(B,$thf( q ))]]) ).
thf(2724,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)],[2546,90]) ).
thf(2725,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)],[2724]) ).
thf(2726,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2725:[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(2743,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ implies ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2726]) ).
thf(12261,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4173,170]) ).
thf(12262,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12261]) ).
thf(12263,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12262:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( K )),bind(D,$thf( K @ ( K @ and ) @ ( K @ implies ) @ ( F @ implies ) )),bind(E,$thf( A ))]]) ).
thf(12563,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12263]) ).
thf(248,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[47,191]) ).
thf(249,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[248]) ).
thf(250,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ or ) @ implies ) )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[249]) ).
thf(186,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ( ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( B @ not @ ( A @ implies ) @ not @ equivalent ) )
!= ( D @ ( C @ implies ) @ ( D @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,89]) ).
thf(187,plain,
! [B: $i,A: $i] :
( ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) )
!= ( B @ ( A @ implies ) @ ( B @ implies ) ) ),
inference(pattern_uni,[status(thm)],[186:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(231,plain,
! [B: $i,A: $i] :
( ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) )
!= ( B @ ( A @ implies ) @ ( B @ implies ) ) ),
inference(simp,[status(thm)],[187]) ).
thf(3624,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ ( r @ not @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ ( B @ not @ ( A @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,3487]) ).
thf(3625,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ implies ) @ ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ and ) @ theorem ),
inference(pattern_uni,[status(thm)],[3624:[bind(A,$thf( r @ not )),bind(B,$thf( q ))]]) ).
thf(194,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( r @ not ) )
| ~ ( q @ not @ ( B @ ( A @ and ) @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,13]) ).
thf(218,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) )
!= r )
| ~ ( q @ not @ ( B @ ( A @ and ) @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[194]) ).
thf(12290,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ ( F @ or ) @ theorem ) )
| ~ $true
| ( F @ ( E @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4187,170]) ).
thf(12291,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( E @ ( F @ or ) @ theorem ) )
| ( F @ ( E @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12290]) ).
thf(12292,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12291:[bind(A,$thf( A )),bind(B,$thf( G )),bind(C,$thf( K )),bind(D,$thf( L )),bind(E,$thf( L @ ( K @ or ) @ ( L @ implies ) @ ( G @ implies ) )),bind(F,$thf( A ))]]) ).
thf(12527,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( A @ ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12292]) ).
thf(12211,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ equivalent ) @ ( B @ ( B @ implies ) @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ~ $true
| ( D @ ( C @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4188,170]) ).
thf(12212,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ equivalent ) @ ( B @ ( B @ implies ) @ implies ) @ ( A @ or ) @ theorem )
!= ( C @ ( D @ or ) @ theorem ) )
| ( D @ ( C @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12211]) ).
thf(12213,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ equivalent ) @ ( B @ ( B @ implies ) @ implies ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12212:[bind(A,$thf( A )),bind(B,$thf( J )),bind(C,$thf( J @ ( J @ equivalent ) @ ( J @ ( J @ implies ) @ implies ) )),bind(D,$thf( A ))]]) ).
thf(12552,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ equivalent ) @ ( B @ ( B @ implies ) @ implies ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12213]) ).
thf(5736,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ( ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( B @ not @ ( A @ implies ) @ not @ equivalent ) )
!= ( C @ ( D @ implies ) ) )
| ~ ( C @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,5020]) ).
thf(5737,plain,
! [B: $i,A: $i] :
( ( ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) )
!= ( A @ ( B @ implies ) ) )
| ~ ( A @ theorem ) ),
inference(pattern_uni,[status(thm)],[5736:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(5813,plain,
! [B: $i,A: $i] :
( ( ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) )
!= ( A @ ( B @ implies ) ) )
| ~ ( A @ theorem ) ),
inference(simp,[status(thm)],[5737]) ).
thf(13667,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ or ) @ ( C @ implies ) @ or ) @ theorem )
!= ( E @ theorem ) )
| ~ $true
| ( E @ ( D @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[12553,90]) ).
thf(13668,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ or ) @ ( C @ implies ) @ or ) @ theorem )
!= ( E @ theorem ) )
| ( E @ ( D @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[13667]) ).
thf(13669,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ or ) @ ( D @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[13668:[bind(A,$thf( G )),bind(B,$thf( J )),bind(C,$thf( K )),bind(D,$thf( D )),bind(E,$thf( G @ ( K @ ( J @ or ) @ ( K @ implies ) @ or ) ))]]) ).
thf(13721,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( B @ ( D @ ( C @ or ) @ ( D @ implies ) @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[13669]) ).
thf(2456,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[90,243]) ).
thf(2457,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2456]) ).
thf(2526,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ implies ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[2457]) ).
thf(139,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ not @ or ) )
!= ( E @ ( C @ or ) ) )
| ( B @ ( A @ implies ) @ ( D @ or ) @ ( E @ ( D @ or ) @ ( C @ or ) @ implies ) @ axiom ) ),
inference(paramod_ordered,[status(thm)],[20,17]) ).
thf(140,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ implies ) @ ( B @ or ) @ ( A @ ( B @ or ) @ ( C @ not @ or ) @ implies ) @ axiom ),
inference(pattern_uni,[status(thm)],[139:[bind(A,$thf( F )),bind(B,$thf( B )),bind(C,$thf( F @ not )),bind(D,$thf( D )),bind(E,$thf( B ))]]) ).
thf(151,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ implies ) @ ( B @ or ) @ ( A @ ( B @ or ) @ ( C @ not @ or ) @ implies ) @ axiom ),
inference(simp,[status(thm)],[140]) ).
thf(10695,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ implies ) @ ( B @ or ) @ ( A @ ( B @ or ) @ ( C @ implies ) @ implies ) @ axiom ),
inference(rewrite,[status(thm)],[151,20]) ).
thf(2661,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)],[2545,90]) ).
thf(2662,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)],[2661]) ).
thf(2663,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2662:[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(2680,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ or ) @ ( D @ implies ) @ ( B @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2663]) ).
thf(1512,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( B @ not @ ( A @ implies ) @ not @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[175,1312]) ).
thf(1513,plain,
~ ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[1512:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) ))]]) ).
thf(188,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( r @ not ) )
| ( ( q @ not @ ( B @ ( A @ and ) @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( D @ ( C @ implies ) @ ( D @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,89]) ).
thf(214,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) )
!= r )
| ( ( q @ not @ ( B @ ( A @ and ) @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( D @ ( C @ implies ) @ ( D @ implies ) ) ) ),
inference(simp,[status(thm)],[188]) ).
thf(36,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ implies ) @ theorem )
!= ( B @ theorem ) )
| ~ ( B @ theorem )
| ( A @ theorem ) ),
inference(simp,[status(thm)],[35]) ).
thf(4068,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true
| ~ ( B @ theorem ) ),
inference(paramod_ordered,[status(thm)],[107,191]) ).
thf(4069,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) @ theorem )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[4068]) ).
thf(4146,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ or ) )
!= ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) )
| ~ ( B @ theorem ) ),
inference(simp,[status(thm)],[4069]) ).
thf(2222,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ and ) @ ( A @ implies ) @ not )
!= ( r @ ( q @ implies ) @ ( p @ and ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ implies ) @ not ) )
| ~ ( C @ not @ ( B @ implies ) @ ( A @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ) ),
inference(paramod_ordered,[status(thm)],[220,1500]) ).
thf(2223,plain,
~ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ and ) @ ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ implies ) @ implies ) @ not @ theorem ),
inference(pattern_uni,[status(thm)],[2222:[bind(A,$thf( q @ ( r @ not @ and ) @ ( p @ implies ) @ not )),bind(B,$thf( p )),bind(C,$thf( r @ ( q @ implies ) ))]]) ).
thf(13835,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ ( A @ ( A @ or ) @ equivalent ) @ theorem )
!= ( C @ theorem ) )
| ~ $true
| ( C @ ( B @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[13388,90]) ).
thf(13836,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ or ) @ ( A @ ( A @ or ) @ equivalent ) @ theorem )
!= ( C @ theorem ) )
| ( C @ ( B @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[13835]) ).
thf(13837,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ ( B @ ( B @ or ) @ equivalent ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[13836:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ ( I @ or ) @ ( I @ ( I @ or ) @ equivalent ) ))]]) ).
thf(13877,plain,
! [B: $i,A: $i] : ( B @ ( B @ or ) @ ( B @ ( B @ or ) @ equivalent ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[13837]) ).
thf(12309,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4163,170]) ).
thf(12310,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12309]) ).
thf(12311,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12310:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( I )),bind(D,$thf( I @ ( I @ ( I @ or ) @ implies ) @ ( F @ or ) )),bind(E,$thf( A ))]]) ).
thf(12530,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( C @ ( C @ or ) @ implies ) @ ( B @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12311]) ).
thf(12350,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ~ $true
| ( E @ ( D @ or ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4273,170]) ).
thf(12351,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ or ) @ ( A @ or ) @ theorem )
!= ( D @ ( E @ or ) @ theorem ) )
| ( E @ ( D @ or ) @ theorem ) ),
inference(simp,[status(thm)],[12350]) ).
thf(12352,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ or ) @ or ) @ theorem ),
inference(pattern_uni,[status(thm)],[12351:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( K )),bind(D,$thf( K @ ( K @ and ) @ ( K @ implies ) @ ( F @ or ) )),bind(E,$thf( A ))]]) ).
thf(12535,plain,
! [C: $i,B: $i,A: $i] : ( A @ ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ or ) @ or ) @ theorem ),
inference(simp,[status(thm)],[12352]) ).
thf(2097,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,1641]) ).
thf(2098,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[2097:[bind(A,$thf( F )),bind(B,$thf( F @ not )),bind(C,$thf( C )),bind(D,$thf( F @ not ))]]) ).
thf(2138,plain,
! [B: $i,A: $i] : ( B @ not @ ( B @ not @ ( B @ implies ) @ implies ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[2098]) ).
thf(127,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(128,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)],[127]) ).
thf(129,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)],[128:[bind(A,$thf( I )),bind(B,$thf( B )),bind(C,$thf( I @ not @ ( I @ not @ ( I @ implies ) @ implies ) ))]]) ).
thf(131,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)],[129]) ).
thf(178,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) ) )
| ( ( B @ not @ ( A @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( D @ ( C @ or ) @ ( D @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,106]) ).
thf(179,plain,
! [B: $i,A: $i] :
( ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( B @ ( A @ or ) @ ( B @ implies ) ) ),
inference(pattern_uni,[status(thm)],[178:[bind(A,$thf( p )),bind(B,$thf( q @ not @ ( r @ not @ implies ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(227,plain,
! [B: $i,A: $i] :
( ( q @ not @ ( r @ not @ implies ) @ not @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( B @ ( A @ or ) @ ( B @ implies ) ) ),
inference(simp,[status(thm)],[179]) ).
thf(4250,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ~ $true
| ( D @ ( C @ implies ) @ theorem ) ),
inference(paramod_ordered,[status(thm)],[4174,90]) ).
thf(4251,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ and ) @ ( B @ implies ) @ ( A @ or ) @ theorem )
!= ( D @ theorem ) )
| ( D @ ( C @ implies ) @ theorem ) ),
inference(simp,[status(thm)],[4250]) ).
thf(4252,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(pattern_uni,[status(thm)],[4251:[bind(A,$thf( E )),bind(B,$thf( J )),bind(C,$thf( C )),bind(D,$thf( J @ ( J @ and ) @ ( J @ implies ) @ ( E @ or ) ))]]) ).
thf(4274,plain,
! [C: $i,B: $i,A: $i] : ( C @ ( C @ and ) @ ( C @ implies ) @ ( B @ or ) @ ( A @ implies ) @ theorem ),
inference(simp,[status(thm)],[4252]) ).
thf(203,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) @ not )
!= ( q @ not ) )
| ( ( B @ ( A @ and ) @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( C @ ( D @ implies ) @ ( C @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,136]) ).
thf(215,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ not @ ( A @ implies ) )
!= q )
| ( ( B @ ( A @ and ) @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) )
!= ( C @ ( D @ implies ) @ ( C @ implies ) ) ) ),
inference(simp,[status(thm)],[203]) ).
thf(3148,plain,
! [B: $i,A: $i] :
( ( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[3127,243]) ).
thf(3149,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ implies ) @ or ) @ theorem )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) @ theorem ) ),
inference(simp,[status(thm)],[3148]) ).
thf(3200,plain,
! [B: $i,A: $i] :
( ( B @ not @ ( B @ ( A @ implies ) @ or ) )
!= ( q @ ( r @ not @ and ) @ ( p @ implies ) @ not @ ( r @ ( q @ implies ) @ ( p @ and ) @ equivalent ) ) ),
inference(simp,[status(thm)],[3149]) ).
thf(200,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ and ) )
!= ( r @ ( q @ implies ) @ ( p @ and ) ) )
| ( ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( B @ not @ ( A @ implies ) @ not @ equivalent ) )
!= ( C @ ( D @ implies ) @ ( C @ implies ) ) ) ),
inference(paramod_ordered,[status(thm)],[175,136]) ).
thf(201,plain,
! [B: $i,A: $i] :
( ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) )
!= ( A @ ( B @ implies ) @ ( A @ implies ) ) ),
inference(pattern_uni,[status(thm)],[200:[bind(A,$thf( p )),bind(B,$thf( r @ ( q @ implies ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(222,plain,
! [B: $i,A: $i] :
( ( q @ not @ ( r @ not @ implies ) @ ( p @ and ) @ ( r @ ( q @ implies ) @ not @ ( p @ implies ) @ not @ equivalent ) )
!= ( A @ ( B @ implies ) @ ( A @ implies ) ) ),
inference(simp,[status(thm)],[201]) ).
thf(34827,plain,
$false,
inference(e,[status(thm)],[2199,4188,2306,16808,1686,4183,333,170,217,3285,2527,12539,13548,14602,3481,1640,174,16491,2548,24,37,2531,25,1835,16994,4156,5269,14,12718,4654,3617,20,4179,13388,228,1641,1815,5020,216,5957,4173,376,106,3621,2540,221,132,243,312,89,133,23332,1338,220,1768,5281,13547,12542,12561,24197,2541,1519,12550,28,1502,4499,33,275,21,92,229,65,6708,1819,4187,2547,224,252,1837,13116,12538,12546,169,109,14623,225,339,193,6539,212,2519,1831,13,12533,4152,1759,3215,4163,4148,237,1814,2546,12553,1515,22233,2529,34,6546,17,279,64,2524,149,4144,1833,22,5395,2525,1752,118,27,6493,191,21413,12541,12,445,4186,2308,1312,3123,49,3487,3619,4149,4171,4273,5158,2079,172,219,274,230,76,12537,4154,4176,4374,2197,13876,2538,1853,5367,2610,2314,213,91,66,5392,108,12551,12534,278,4373,223,299,226,1694,12557,5812,3206,16024,13117,48,63,3507,18,11611,3129,67,16,2545,1813,1637,12720,1763,3127,12540,15828,336,1504,175,23774,539,1817,2310,495,1517,2743,12563,250,231,3625,218,12527,1639,5382,12552,5813,171,13721,2526,23,75,4153,10695,1706,2680,1513,214,36,262,19,4146,107,136,13377,2223,13877,12530,1500,15,14603,12535,2138,131,47,13720,90,227,4274,2206,215,3200,222,4174]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL266-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.15 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.13/0.46 % Computer : n011.cluster.edu
% 0.13/0.46 % Model : x86_64 x86_64
% 0.13/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.46 % Memory : 8046.5625MB
% 0.13/0.46 % OS : Linux 6.8.0-71-generic
% 0.13/0.46 % CPULimit : 300
% 0.13/0.46 % WCLimit : 300
% 0.13/0.46 % DateTime : Fri Sep 25 22:09:29 UTC 2026
% 0.13/0.46 % CPUTime :
% 0.13/0.46 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.70/1.12 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.09/1.36 % [INFO] Parsing done (233ms).
% 1.09/1.38 % [INFO] Running in sequential loop mode.
% 1.94/1.93 % [INFO] eprover registered as external prover.
% 1.94/1.95 % [INFO] Scanning for conjecture ...
% 2.09/2.07 % [INFO] Found a conjecture (or negated_conjecture) and 10 axioms. Running axiom selection ...
% 2.09/2.11 % [INFO] Axiom selection finished. Selected 10 axioms (removed 0 axioms).
% 2.09/2.15 % [INFO] Problem is propositional (TPTP CNF).
% 2.28/2.16 % [INFO] Type checking passed.
% 2.28/2.16 % [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 ...
% 128.13/39.04 % External prover 'e' found a proof!
% 128.13/39.04 % [INFO] Killing All external provers ...
% 128.13/39.04 % Time passed: 38353ms (effective reasoning time: 37651ms)
% 128.13/39.05 % 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
% 128.13/39.05 % No. of inferences in proof: 788
% 128.13/39.05 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 38353 ms resp. 37651 ms w/o parsing
% 130.46/39.44 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 130.46/39.45 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------