%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LCL895+1 : TPTP v9.3.1. Released v5.5.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 : n004.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:53:19 AM UTC 2026
% Result : Theorem 149.63s 44.64s
% Output : Refutation 137.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 115
% Number of leaves : 9
% Syntax : Number of formulae : 614 ( 212 unt; 0 typ; 0 def)
% Number of atoms : 1401 (1039 equ; 0 cnn)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 5985 ( 698 ~; 754 |; 9 &;4520 @)
% ( 2 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 10 ( 7 usr; 7 con; 0-2 aty)
% Number of variables : 955 ( 0 ^; 955 !; 0 ?; 955 :)
% Comments :
%------------------------------------------------------------------------------
thf('==>_decl',type,
'==>': $i > $i > $i ).
thf(c_decl,type,
c: $i ).
thf(a_decl,type,
a: $i ).
thf('0_decl',type,
'0': $i ).
thf(b_decl,type,
b: $i ).
thf('+_decl',type,
'+': $i > $i > $i ).
thf(sk1_decl,type,
sk1: $o ).
thf(1,conjecture,
( ( ( ( b @ ( c @ '==>' ) )
= '0' )
& ( ( a @ ( c @ '==>' ) )
= '0' ) )
<=> ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_09) ).
thf(2,negated_conjecture,
~ ( ( ( ( b @ ( c @ '==>' ) )
= '0' )
& ( ( a @ ( c @ '==>' ) )
= '0' ) )
<=> ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(11,plain,
~ ( ( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' )
=> ( ( ( b @ ( c @ '==>' ) )
= '0' )
& ( ( a @ ( c @ '==>' ) )
= '0' ) ) )
& ( ( ( ( b @ ( c @ '==>' ) )
= '0' )
& ( ( a @ ( c @ '==>' ) )
= '0' ) )
=> ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(12,plain,
( ( ( ( b @ ( c @ '==>' ) )
!= '0' )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 )
& ( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' )
| sk1 )
& ( ~ sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= '0' ) )
& ( ~ sk1
| ( ( b @ ( c @ '==>' ) )
= '0' ) )
& ( ~ sk1
| ( ( a @ ( c @ '==>' ) )
= '0' ) ) ),
inference(cnf,[status(esa)],[11]) ).
thf(16,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' )
| sk1 ),
inference(cnfConj,[status(thm)],[12]) ).
thf(21,plain,
( sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(lifteq,[status(thm)],[16]) ).
thf(9,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
= ( C @ ( B @ '==>' ) @ ( A @ '==>' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_07) ).
thf(41,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
= ( C @ ( B @ '==>' ) @ ( A @ '==>' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(42,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
= ( C @ ( B @ '==>' ) @ ( A @ '==>' ) ) ),
inference(cnf,[status(esa)],[41]) ).
thf(43,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
= ( C @ ( B @ '==>' ) @ ( A @ '==>' ) ) ),
inference(lifteq,[status(thm)],[42]) ).
thf(10,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
= ( A @ ( B @ '==>' ) @ ( B @ '+' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_08) ).
thf(44,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
= ( A @ ( B @ '==>' ) @ ( B @ '+' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(45,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
= ( A @ ( B @ '==>' ) @ ( B @ '+' ) ) ),
inference(cnf,[status(esa)],[44]) ).
thf(46,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
= ( A @ ( B @ '==>' ) @ ( B @ '+' ) ) ),
inference(lifteq,[status(thm)],[45]) ).
thf(542,plain,
! [B: $i,A: $i] :
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( B @ ( A @ '==>' ) ) )
| ( ( '0' @ ( A @ '+' ) )
= ( A @ ( B @ '==>' ) @ ( B @ '+' ) ) )
| sk1 ),
inference(paramod_ordered,[status(thm)],[21,46]) ).
thf(543,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '+' ) )
= ( '0' @ ( c @ '+' ) ) )
| sk1 ),
inference(pattern_uni,[status(thm)],[542:[bind(A,$thf( c )),bind(B,$thf( b @ ( a @ '==>' ) @ ( a @ '+' ) ))]]) ).
thf(3,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
= ( C @ ( B @ '+' ) @ ( A @ '+' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_01) ).
thf(23,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
= ( C @ ( B @ '+' ) @ ( A @ '+' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(24,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
= ( C @ ( B @ '+' ) @ ( A @ '+' ) ) ),
inference(cnf,[status(esa)],[23]) ).
thf(25,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
= ( C @ ( B @ '+' ) @ ( A @ '+' ) ) ),
inference(lifteq,[status(thm)],[24]) ).
thf(5,axiom,
! [A: $i] :
( ( '0' @ ( A @ '+' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_03) ).
thf(29,plain,
! [A: $i] :
( ( '0' @ ( A @ '+' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(30,plain,
! [A: $i] :
( ( '0' @ ( A @ '+' ) )
= A ),
inference(cnf,[status(esa)],[29]) ).
thf(31,plain,
! [A: $i] :
( ( '0' @ ( A @ '+' ) )
= A ),
inference(lifteq,[status(thm)],[30]) ).
thf(581,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[543,25,31]) ).
thf(599,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) ) )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[43,581]) ).
thf(600,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(pattern_uni,[status(thm)],[599:[bind(A,$thf( a )),bind(B,$thf( b @ ( a @ '==>' ) )),bind(C,$thf( c ))]]) ).
thf(816,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( '0' @ '+' ) @ ( a @ '+' ) )
= c )
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[21,600]) ).
thf(817,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( '0' @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[816]) ).
thf(841,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= b )
| ( a != c )
| ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( '0' @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[817]) ).
thf(4,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ '+' ) )
= ( A @ ( B @ '+' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_02) ).
thf(26,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ '+' ) )
= ( A @ ( B @ '+' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(27,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ '+' ) )
= ( A @ ( B @ '+' ) ) ),
inference(cnf,[status(esa)],[26]) ).
thf(28,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ '+' ) )
= ( A @ ( B @ '+' ) ) ),
inference(lifteq,[status(thm)],[27]) ).
thf(240,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= ( '0' @ ( C @ '+' ) ) )
| ( ( A @ ( B @ '+' ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[28,31]) ).
thf(241,plain,
! [A: $i] :
( ( A @ ( '0' @ '+' ) )
= A ),
inference(pattern_uni,[status(thm)],[240:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( A ))]]) ).
thf(67061,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= b )
| ( a != c )
| ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[841,241]) ).
thf(594,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '+' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) ) )
| ( ( A @ ( a @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[31,581]) ).
thf(682,plain,
! [A: $i] :
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) )
!= '0' )
| ( A
!= ( b @ ( a @ '==>' ) ) )
| ( ( A @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[594]) ).
thf(716,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) )
!= '0' )
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[682]) ).
thf(59383,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) )
!= '0' )
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[716,43]) ).
thf(6,axiom,
! [A: $i] :
( ( A @ ( A @ '==>' ) )
= '0' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_04) ).
thf(32,plain,
! [A: $i] :
( ( A @ ( A @ '==>' ) )
= '0' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(33,plain,
! [A: $i] :
( ( A @ ( A @ '==>' ) )
= '0' ),
inference(cnf,[status(esa)],[32]) ).
thf(34,plain,
! [A: $i] :
( ( A @ ( A @ '==>' ) )
= '0' ),
inference(lifteq,[status(thm)],[33]) ).
thf(412,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= ( D @ ( C @ '+' ) ) )
| ( ( E @ ( A @ ( B @ '+' ) @ '==>' ) )
= ( E @ ( D @ '==>' ) @ ( C @ '==>' ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,43]) ).
thf(413,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ '+' ) @ '==>' ) )
= ( C @ ( B @ '==>' ) @ ( A @ '==>' ) ) ),
inference(pattern_uni,[status(thm)],[412:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(441,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ '+' ) @ '==>' ) )
= ( C @ ( B @ '==>' ) @ ( A @ '==>' ) ) ),
inference(simp,[status(thm)],[413]) ).
thf(5234,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ '==>' ) @ ( B @ '==>' ) )
= ( C @ ( B @ '==>' ) @ ( A @ '==>' ) ) ),
inference(rewrite,[status(thm)],[441,43]) ).
thf(5261,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ '==>' ) )
!= ( D @ ( C @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) )
= ( D @ ( B @ '==>' ) @ ( C @ '==>' ) ) ) ),
inference(paramod_ordered,[status(thm)],[34,5234]) ).
thf(5262,plain,
! [B: $i,A: $i] :
( ( '0' @ ( B @ '==>' ) )
= ( A @ ( B @ '==>' ) @ ( A @ '==>' ) ) ),
inference(pattern_uni,[status(thm)],[5261:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( A ))]]) ).
thf(7,axiom,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_05) ).
thf(35,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(36,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(cnf,[status(esa)],[35]) ).
thf(37,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(lifteq,[status(thm)],[36]) ).
thf(6166,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[5262,37]) ).
thf(13,plain,
( ~ sk1
| ( ( a @ ( c @ '==>' ) )
= '0' ) ),
inference(cnfConj,[status(thm)],[12]) ).
thf(19,plain,
( ~ sk1
| ( ( a @ ( c @ '==>' ) )
= '0' ) ),
inference(lifteq,[status(thm)],[13]) ).
thf(14,plain,
( ~ sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= '0' ) ),
inference(cnfConj,[status(thm)],[12]) ).
thf(18,plain,
( ~ sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= '0' ) ),
inference(lifteq,[status(thm)],[14]) ).
thf(143,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ~ sk1
| ( '0' != '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[19,18]) ).
thf(144,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[143]) ).
thf(153,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= a )
| ( c != c )
| ~ sk1 ),
inference(simp,[status(thm)],[144]) ).
thf(158,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= a )
| ~ sk1 ),
inference(simp,[status(thm)],[153]) ).
thf(918,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '+' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ( A != a )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[31,158]) ).
thf(944,plain,
( ( ( b @ ( a @ '==>' ) )
!= '0' )
| ( a != a )
| ~ sk1 ),
inference(simp,[status(thm)],[918]) ).
thf(951,plain,
( ( ( b @ ( a @ '==>' ) )
!= '0' )
| ~ sk1 ),
inference(simp,[status(thm)],[944]) ).
thf(6278,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ '==>' ) @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( '0' != '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[6166,951]) ).
thf(6279,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ '==>' ) @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[6278]) ).
thf(6345,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ '==>' ) )
!= b )
| ( A != a )
| ~ sk1 ),
inference(simp,[status(thm)],[6279]) ).
thf(6405,plain,
! [A: $i] :
( ( ( a @ ( A @ '==>' ) )
!= b )
| ~ sk1 ),
inference(simp,[status(thm)],[6345]) ).
thf(331,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ~ sk1
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) @ ( c @ '==>' ) )
!= '0' ) ),
inference(paramod_ordered,[status(thm)],[25,18]) ).
thf(358,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( b @ ( a @ '==>' ) ) )
| ( ( B @ ( A @ '+' ) )
!= a )
| ~ sk1
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) @ ( c @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[331]) ).
thf(365,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ~ sk1
| ( ( b @ ( a @ '==>' ) @ ( B @ '+' ) @ ( A @ '+' ) @ ( c @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[358]) ).
thf(352,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ '+' ) )
!= ( D @ ( C @ '+' ) ) )
| ( ( E @ ( B @ ( A @ '+' ) @ '+' ) )
= ( E @ ( D @ '+' ) @ ( C @ '+' ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,25]) ).
thf(353,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
= ( C @ ( A @ '+' ) @ ( B @ '+' ) ) ),
inference(pattern_uni,[status(thm)],[352:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(361,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
= ( C @ ( A @ '+' ) @ ( B @ '+' ) ) ),
inference(simp,[status(thm)],[353]) ).
thf(3285,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ '+' ) @ ( A @ '+' ) )
= ( C @ ( A @ '+' ) @ ( B @ '+' ) ) ),
inference(rewrite,[status(thm)],[361,25]) ).
thf(5253,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ '==>' ) @ ( B @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[5234,34]) ).
thf(5254,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ '==>' ) @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[5253:[bind(A,$thf( E )),bind(B,$thf( F @ ( E @ '==>' ) )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ '==>' ) ))]]) ).
thf(5639,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ '==>' ) @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[5254]) ).
thf(8232,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ '==>' ) @ ( A @ '==>' ) )
!= ( D @ ( C @ '==>' ) ) )
| ( ( D @ ( '0' @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[6166,5639]) ).
thf(8233,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ '==>' ) @ ( '0' @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[8232:[bind(A,$thf( F )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ '==>' ) ))]]) ).
thf(8331,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ '==>' ) @ ( '0' @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[8233]) ).
thf(8,axiom,
! [A: $i] :
( ( A @ ( '0' @ '==>' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_06) ).
thf(38,plain,
! [A: $i] :
( ( A @ ( '0' @ '==>' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(39,plain,
! [A: $i] :
( ( A @ ( '0' @ '==>' ) )
= A ),
inference(cnf,[status(esa)],[38]) ).
thf(40,plain,
! [A: $i] :
( ( A @ ( '0' @ '==>' ) )
= A ),
inference(lifteq,[status(thm)],[39]) ).
thf(8605,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[8331,40]) ).
thf(597,plain,
! [C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
!= ( B @ ( A @ '+' ) ) )
| ( ( C @ ( c @ '==>' ) )
= ( C @ ( B @ '==>' ) @ ( A @ '==>' ) ) )
| sk1 ),
inference(paramod_ordered,[status(thm)],[581,43]) ).
thf(598,plain,
! [A: $i] :
( ( ( A @ ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ '==>' ) @ ( a @ '==>' ) )
= ( A @ ( c @ '==>' ) ) )
| sk1 ),
inference(pattern_uni,[status(thm)],[597:[bind(A,$thf( a )),bind(B,$thf( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) )),bind(C,$thf( C ))]]) ).
thf(697,plain,
! [A: $i] :
( ( ( A @ ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ '==>' ) @ ( a @ '==>' ) )
= ( A @ ( c @ '==>' ) ) )
| sk1 ),
inference(simp,[status(thm)],[598]) ).
thf(410,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
!= ( E @ ( D @ '+' ) ) )
| ( ( F @ ( C @ ( B @ '+' ) @ ( A @ '+' ) @ '==>' ) )
= ( F @ ( E @ '==>' ) @ ( D @ '==>' ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,43]) ).
thf(411,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ '+' ) @ ( C @ '+' ) @ '==>' ) )
= ( B @ ( A @ '==>' ) @ ( D @ ( C @ '+' ) @ '==>' ) ) ),
inference(pattern_uni,[status(thm)],[410:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ '+' ) )),bind(E,$thf( C ))]]) ).
thf(440,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ '+' ) @ ( C @ '+' ) @ '==>' ) )
= ( B @ ( A @ '==>' ) @ ( D @ ( C @ '+' ) @ '==>' ) ) ),
inference(simp,[status(thm)],[411]) ).
thf(13557,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ '+' ) @ '==>' ) @ ( C @ '==>' ) )
= ( B @ ( A @ '==>' ) @ ( D @ '==>' ) @ ( C @ '==>' ) ) ),
inference(rewrite,[status(thm)],[440,43]) ).
thf(41785,plain,
! [A: $i] :
( ( ( A @ ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) )
= ( A @ ( c @ '==>' ) ) )
| sk1 ),
inference(rewrite,[status(thm)],[697,13557]) ).
thf(42142,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ '==>' ) @ ( B @ '==>' ) )
!= ( C @ ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '==>' ) ) )
| ( ( '0' @ ( a @ '==>' ) )
= ( C @ ( c @ '==>' ) ) )
| sk1 ),
inference(paramod_ordered,[status(thm)],[8605,41785]) ).
thf(42143,plain,
( ( ( '0' @ ( a @ '==>' ) )
= ( b @ ( a @ '==>' ) @ ( c @ '==>' ) ) )
| sk1 ),
inference(pattern_uni,[status(thm)],[42142:[bind(A,$thf( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) )),bind(B,$thf( b @ ( a @ '==>' ) )),bind(C,$thf( b @ ( a @ '==>' ) ))]]) ).
thf(6177,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ '==>' ) @ ( A @ '==>' ) )
!= ( E @ ( C @ '==>' ) @ ( D @ '==>' ) ) )
| ( ( E @ ( D @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[6166,5234]) ).
thf(6178,plain,
! [B: $i,A: $i] :
( ( A @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[6177:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A )),bind(E,$thf( A ))]]) ).
thf(6956,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ '==>' ) @ ( B @ '==>' ) )
!= ( E @ ( D @ ( C @ '+' ) @ '==>' ) ) )
| ( ( E @ ( D @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[6178,43]) ).
thf(6957,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( C @ '==>' ) @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[6956:[bind(A,$thf( I )),bind(B,$thf( G @ ( F @ '+' ) )),bind(C,$thf( F )),bind(D,$thf( G )),bind(E,$thf( I @ ( I @ '==>' ) ))]]) ).
thf(7070,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( C @ '==>' ) @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[6957]) ).
thf(15467,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ '==>' ) @ ( B @ '==>' ) )
!= ( F @ ( F @ '==>' ) @ ( E @ '==>' ) ) )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( D @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[5234,7070]) ).
thf(15468,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ '==>' ) @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[15467:[bind(A,$thf( C )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( B )),bind(F,$thf( C ))]]) ).
thf(15796,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ '==>' ) @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[15468]) ).
thf(19622,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[15796,8605]) ).
thf(15455,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ '==>' ) @ ( B @ '==>' ) @ ( A @ '==>' ) )
!= ( F @ ( D @ '==>' ) @ ( E @ '==>' ) ) )
| ( ( F @ ( E @ '==>' ) @ ( D @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[7070,5234]) ).
thf(15456,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( C @ '==>' ) @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[15455:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( H )),bind(D,$thf( B )),bind(E,$thf( A )),bind(F,$thf( H @ ( H @ '==>' ) ))]]) ).
thf(15790,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( C @ '==>' ) @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[15456]) ).
thf(19798,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[19622,15790]) ).
thf(19799,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[19798:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(19953,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[19799]) ).
thf(6288,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( D @ ( E @ '==>' ) ) )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( D @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[43,6166]) ).
thf(6289,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ '==>' ) @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[6288:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( G @ ( F @ '+' ) ))]]) ).
thf(6371,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ '==>' ) @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[6289]) ).
thf(19695,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[19622,6371]) ).
thf(19696,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[19695:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(20051,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[19696]) ).
thf(20197,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[20051,40]) ).
thf(21177,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[19953,20197]) ).
thf(21353,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[21177,15790]) ).
thf(21354,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[21353:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(21513,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[21354]) ).
thf(20370,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[20197,15790]) ).
thf(20371,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[20370:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(20566,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[20371]) ).
thf(21246,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[21177,6371]) ).
thf(21247,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[21246:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(21612,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[21247]) ).
thf(21630,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[21612,40]) ).
thf(22682,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[20566,21630]) ).
thf(22751,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[22682,6371]) ).
thf(22752,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[22751:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(23115,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[22752]) ).
thf(23482,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[23115,40]) ).
thf(24944,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[21513,23482]) ).
thf(25131,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[24944,15790]) ).
thf(25132,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[25131:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(25289,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[25132]) ).
thf(23665,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[23482,15790]) ).
thf(23666,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[23665:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(23838,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[23666]) ).
thf(22864,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[22682,15790]) ).
thf(22865,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[22864:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(23022,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[22865]) ).
thf(21806,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[21630,15790]) ).
thf(21807,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[21806:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(21960,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[21807]) ).
thf(25016,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[24944,6371]) ).
thf(25017,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[25016:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(25380,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[25017]) ).
thf(26502,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[25380,40]) ).
thf(28019,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[21960,26502]) ).
thf(28094,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[28019,6371]) ).
thf(28095,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[28094:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(28463,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[28095]) ).
thf(28505,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[28463,40]) ).
thf(29423,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[23022,28505]) ).
thf(29490,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[29423,6371]) ).
thf(29491,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[29490:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(29809,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[29491]) ).
thf(29874,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[29809,40]) ).
thf(30835,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[23838,29874]) ).
thf(30902,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[30835,6371]) ).
thf(30903,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[30902:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(31260,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[30903]) ).
thf(31380,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[31260,40]) ).
thf(33638,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[25289,31380]) ).
thf(33704,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[33638,6371]) ).
thf(33705,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[33704:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(34069,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[33705]) ).
thf(34133,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[34069,40]) ).
thf(34330,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[34133,15790]) ).
thf(34331,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[34330:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(34493,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[34331]) ).
thf(33835,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[33638,15790]) ).
thf(33836,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[33835:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(33999,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[33836]) ).
thf(31565,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[31380,15790]) ).
thf(31566,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[31565:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(31721,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[31566]) ).
thf(31018,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[30835,15790]) ).
thf(31019,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[31018:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(31172,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[31019]) ).
thf(30052,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[29874,15790]) ).
thf(30053,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[30052:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(30209,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[30053]) ).
thf(29601,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[29423,15790]) ).
thf(29602,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[29601:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(29823,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[29602]) ).
thf(28695,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[28505,15790]) ).
thf(28696,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[28695:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(28858,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[28696]) ).
thf(28209,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[28019,15790]) ).
thf(28210,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[28209:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(28373,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[28210]) ).
thf(26688,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[26502,15790]) ).
thf(26689,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[26688:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(26852,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[26689]) ).
thf(35388,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[26852,34133]) ).
thf(35457,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[35388,6371]) ).
thf(35458,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[35457:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(35823,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[35458]) ).
thf(37260,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[35823,40]) ).
thf(39115,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[28373,37260]) ).
thf(39180,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[39115,6371]) ).
thf(39181,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[39180:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(39525,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[39181]) ).
thf(40664,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[39525,40]) ).
thf(41220,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[28858,40664]) ).
thf(41290,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[41220,6371]) ).
thf(41291,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[41290:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(41672,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[41291]) ).
thf(42873,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[41672,40]) ).
thf(44787,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[29823,42873]) ).
thf(44861,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[44787,6371]) ).
thf(44862,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[44861:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(45250,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[44862]) ).
thf(47427,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[45250,40]) ).
thf(50777,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[30209,47427]) ).
thf(50852,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[50777,6371]) ).
thf(50853,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[50852:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(51323,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[50853]) ).
thf(51441,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[51323,40]) ).
thf(52285,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[31172,51441]) ).
thf(52355,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[52285,6371]) ).
thf(52356,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[52355:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(52769,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[52356]) ).
thf(53885,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[52769,40]) ).
thf(56867,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[31721,53885]) ).
thf(56931,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[56867,6371]) ).
thf(56932,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[56931:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(57361,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[56932]) ).
thf(58719,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[57361,40]) ).
thf(60219,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[33999,58719]) ).
thf(60291,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[60219,6371]) ).
thf(60292,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[60291:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(60891,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[60292]) ).
thf(60918,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[60891,40]) ).
thf(62569,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[34493,60918]) ).
thf(62639,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[62569,6371]) ).
thf(62640,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[62639:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(63173,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[62640]) ).
thf(63282,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[63173,40]) ).
thf(63981,plain,
( ( ( b @ ( a @ '==>' ) @ ( c @ '==>' ) )
= '0' )
| sk1 ),
inference(rewrite,[status(thm)],[42143,63282]) ).
thf(64,plain,
! [A: $i] :
( ( ( A @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) ) )
| ~ sk1
| ( '0' != '0' ) ),
inference(paramod_ordered,[status(thm)],[34,18]) ).
thf(65,plain,
! [A: $i] :
( ( ( A @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[64]) ).
thf(71,plain,
! [A: $i] :
( ( A
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ( A != c )
| ~ sk1 ),
inference(simp,[status(thm)],[65]) ).
thf(79,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= c )
| ~ sk1 ),
inference(simp,[status(thm)],[71]) ).
thf(404,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) )
!= c )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[43,79]) ).
thf(425,plain,
! [C: $i,B: $i,A: $i] :
( ( C != b )
| ( ( B @ ( A @ '+' ) )
!= a )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) )
!= c )
| ~ sk1 ),
inference(simp,[status(thm)],[404]) ).
thf(449,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ( ( b @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) )
!= c )
| ~ sk1 ),
inference(simp,[status(thm)],[425]) ).
thf(6950,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ '==>' ) @ ( B @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( '0' != '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[6178,951]) ).
thf(6951,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ '==>' ) @ ( B @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[6950]) ).
thf(7011,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ '==>' ) )
!= b )
| ( B != a )
| ~ sk1 ),
inference(simp,[status(thm)],[6951]) ).
thf(7096,plain,
! [A: $i] :
( ( ( A @ ( A @ '==>' ) )
!= b )
| ~ sk1 ),
inference(simp,[status(thm)],[7011]) ).
thf(107,plain,
! [A: $i] :
( ( ( A @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| sk1
| ( ( '0' @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[34,21]) ).
thf(122,plain,
! [A: $i] :
( ( A != b )
| ( A != a )
| sk1
| ( ( '0' @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[107]) ).
thf(128,plain,
( ( b != a )
| sk1
| ( ( '0' @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[122]) ).
thf(4001,plain,
( ( b != a )
| sk1
| ( ( a @ ( c @ '==>' ) )
= '0' ) ),
inference(rewrite,[status(thm)],[128,31]) ).
thf(17,plain,
( ( ( b @ ( c @ '==>' ) )
!= '0' )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(cnfConj,[status(thm)],[12]) ).
thf(20,plain,
( sk1
| ( ( b @ ( c @ '==>' ) )
!= '0' )
| ( ( a @ ( c @ '==>' ) )
!= '0' ) ),
inference(lifteq,[status(thm)],[17]) ).
thf(218,plain,
( ( '0' != '0' )
| ( ( b @ ( c @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| sk1
| ( ( a @ ( c @ '==>' ) )
!= '0' ) ),
inference(eqfactor_ordered,[status(thm)],[20]) ).
thf(230,plain,
( ( b != a )
| ( c != c )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[218]) ).
thf(235,plain,
( ( b != a )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[230]) ).
thf(4121,plain,
( ( ( a @ ( c @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ( b != a )
| ( '0' != '0' )
| sk1
| ( b != a )
| sk1 ),
inference(paramod_ordered,[status(thm)],[4001,235]) ).
thf(4122,plain,
( ( ( a @ ( c @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ( b != a )
| sk1 ),
inference(simp,[status(thm)],[4121]) ).
thf(4123,plain,
( ( b != a )
| sk1 ),
inference(pattern_uni,[status(thm)],[4122:[]]) ).
thf(1087,plain,
! [A: $i] :
( ( ( A @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( '0' != '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[34,951]) ).
thf(1088,plain,
! [A: $i] :
( ( ( A @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[1087]) ).
thf(1109,plain,
! [A: $i] :
( ( A != b )
| ( A != a )
| ~ sk1 ),
inference(simp,[status(thm)],[1088]) ).
thf(1114,plain,
( ( b != a )
| ~ sk1 ),
inference(simp,[status(thm)],[1109]) ).
thf(4218,plain,
( ( sk1 != sk1 )
| ( b != a )
| ~ $true
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[4123,1114]) ).
thf(4219,plain,
( ( sk1 != sk1 )
| ( b != a ) ),
inference(simp,[status(thm)],[4218]) ).
thf(4220,plain,
b != a,
inference(pattern_uni,[status(thm)],[4219:[]]) ).
thf(41911,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) )
!= ( B @ ( D @ '==>' ) @ ( C @ '==>' ) @ ( B @ '==>' ) ) )
| ( ( A @ ( c @ '==>' ) )
= '0' )
| sk1 ),
inference(paramod_ordered,[status(thm)],[41785,6371]) ).
thf(41912,plain,
( ( ( a @ ( c @ '==>' ) )
= '0' )
| sk1 ),
inference(pattern_uni,[status(thm)],[41911:[bind(A,$thf( a )),bind(B,$thf( a )),bind(C,$thf( b @ ( a @ '==>' ) )),bind(D,$thf( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) ))]]) ).
thf(493,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ '==>' ) @ ( B @ '+' ) )
!= ( '0' @ ( C @ '+' ) ) )
| ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[46,31]) ).
thf(550,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ '==>' ) )
!= '0' )
| ( B != C )
| ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
= C ) ),
inference(simp,[status(thm)],[493]) ).
thf(566,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ '==>' ) )
!= '0' )
| ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
= B ) ),
inference(simp,[status(thm)],[550]) ).
thf(43553,plain,
! [B: $i,A: $i] :
( ( ( a @ ( c @ '==>' ) )
!= ( A @ ( B @ '==>' ) ) )
| ( '0' != '0' )
| ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
= B )
| sk1 ),
inference(paramod_ordered,[status(thm)],[41912,566]) ).
thf(43554,plain,
! [B: $i,A: $i] :
( ( ( a @ ( c @ '==>' ) )
!= ( A @ ( B @ '==>' ) ) )
| ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
= B )
| sk1 ),
inference(simp,[status(thm)],[43553]) ).
thf(43555,plain,
( ( ( c @ ( a @ '==>' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(pattern_uni,[status(thm)],[43554:[bind(A,$thf( a )),bind(B,$thf( c ))]]) ).
thf(617,plain,
! [C: $i,B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
!= ( B @ ( A @ '+' ) ) )
| ( ( C @ ( c @ '+' ) )
= ( C @ ( B @ '+' ) @ ( A @ '+' ) ) )
| sk1 ),
inference(paramod_ordered,[status(thm)],[581,25]) ).
thf(618,plain,
! [A: $i] :
( ( ( A @ ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ '+' ) @ ( a @ '+' ) )
= ( A @ ( c @ '+' ) ) )
| sk1 ),
inference(pattern_uni,[status(thm)],[617:[bind(A,$thf( a )),bind(B,$thf( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) )),bind(C,$thf( C ))]]) ).
thf(715,plain,
! [A: $i] :
( ( ( A @ ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ '+' ) @ ( a @ '+' ) )
= ( A @ ( c @ '+' ) ) )
| sk1 ),
inference(simp,[status(thm)],[618]) ).
thf(340,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
!= ( E @ ( D @ '+' ) ) )
| ( ( F @ ( C @ ( B @ '+' ) @ ( A @ '+' ) @ '+' ) )
= ( F @ ( E @ '+' ) @ ( D @ '+' ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,25]) ).
thf(341,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ '+' ) @ ( C @ '+' ) @ '+' ) )
= ( B @ ( A @ '+' ) @ ( D @ ( C @ '+' ) @ '+' ) ) ),
inference(pattern_uni,[status(thm)],[340:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ '+' ) )),bind(E,$thf( C ))]]) ).
thf(372,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ '+' ) @ ( C @ '+' ) @ '+' ) )
= ( B @ ( A @ '+' ) @ ( D @ ( C @ '+' ) @ '+' ) ) ),
inference(simp,[status(thm)],[341]) ).
thf(13048,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( D @ '+' ) @ '+' ) @ ( C @ '+' ) )
= ( B @ ( A @ '+' ) @ ( D @ '+' ) @ ( C @ '+' ) ) ),
inference(rewrite,[status(thm)],[372,25]) ).
thf(57542,plain,
! [A: $i] :
( ( ( A @ ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ '+' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= ( A @ ( c @ '+' ) ) )
| sk1 ),
inference(rewrite,[status(thm)],[715,13048]) ).
thf(474,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ '==>' ) )
!= ( C @ ( B @ '==>' ) ) )
| ( ( '0' @ ( B @ '+' ) )
= ( B @ ( C @ '==>' ) @ ( C @ '+' ) ) ) ),
inference(paramod_ordered,[status(thm)],[34,46]) ).
thf(475,plain,
! [A: $i] :
( ( A @ ( A @ '==>' ) @ ( A @ '+' ) )
= ( '0' @ ( A @ '+' ) ) ),
inference(pattern_uni,[status(thm)],[474:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(1409,plain,
! [A: $i] :
( ( A @ ( A @ '==>' ) @ ( A @ '+' ) )
= A ),
inference(rewrite,[status(thm)],[475,31]) ).
thf(43483,plain,
( ( ( a @ ( c @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| sk1
| ( ( b @ ( c @ '==>' ) )
!= '0' )
| ( '0' != '0' )
| sk1 ),
inference(paramod_ordered,[status(thm)],[41912,20]) ).
thf(43484,plain,
( ( ( a @ ( c @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ( ( b @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[43483]) ).
thf(43485,plain,
( ( ( b @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(pattern_uni,[status(thm)],[43484:[]]) ).
thf(354,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| sk1
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[25,21]) ).
thf(360,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( b @ ( a @ '==>' ) ) )
| ( ( B @ ( A @ '+' ) )
!= a )
| sk1
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[354]) ).
thf(367,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| sk1
| ( ( b @ ( a @ '==>' ) @ ( B @ '+' ) @ ( A @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[360]) ).
thf(12179,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ '==>' ) @ ( A @ '+' ) )
!= ( C @ ( B @ '+' ) ) )
| ( A != a )
| sk1
| ( ( b @ ( a @ '==>' ) @ ( C @ '+' ) @ ( B @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[1409,367]) ).
thf(12180,plain,
! [A: $i] :
( ( A != a )
| sk1
| ( ( b @ ( a @ '==>' ) @ ( A @ ( A @ '==>' ) @ '+' ) @ ( A @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(pattern_uni,[status(thm)],[12179:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ ( E @ '==>' ) ))]]) ).
thf(12637,plain,
( sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[12180]) ).
thf(14136,plain,
( sk1
| ( ( b @ ( a @ '==>' ) @ ( '0' @ '+' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(rewrite,[status(thm)],[12637,34]) ).
thf(1440,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ '==>' ) @ ( A @ '+' ) )
!= ( C @ ( B @ '+' ) ) )
| ( A
= ( B @ ( C @ '+' ) ) ) ),
inference(paramod_ordered,[status(thm)],[1409,28]) ).
thf(1441,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ '==>' ) @ '+' ) )
= A ),
inference(pattern_uni,[status(thm)],[1440:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ ( E @ '==>' ) ))]]) ).
thf(1526,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ '==>' ) @ '+' ) )
= A ),
inference(simp,[status(thm)],[1441]) ).
thf(12219,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ( A @ '==>' ) @ '+' ) )
!= ( C @ ( B @ '+' ) ) )
| ( A != a )
| sk1
| ( ( b @ ( a @ '==>' ) @ ( C @ '+' ) @ ( B @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[1526,367]) ).
thf(12220,plain,
! [A: $i] :
( ( A != a )
| sk1
| ( ( b @ ( a @ '==>' ) @ ( A @ '+' ) @ ( A @ ( A @ '==>' ) @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(pattern_uni,[status(thm)],[12219:[bind(A,$thf( E )),bind(B,$thf( E @ ( E @ '==>' ) )),bind(C,$thf( E ))]]) ).
thf(12647,plain,
( sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( a @ ( a @ '==>' ) @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[12220]) ).
thf(16240,plain,
( sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( '0' @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(rewrite,[status(thm)],[12647,34]) ).
thf(518,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
!= ( D @ ( C @ '+' ) ) )
| ( ( E @ ( A @ ( B @ '==>' ) @ ( B @ '+' ) @ '+' ) )
= ( E @ ( D @ '+' ) @ ( C @ '+' ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,25]) ).
thf(519,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ '==>' ) @ ( C @ '+' ) @ '+' ) )
= ( A @ ( C @ ( B @ '==>' ) @ '+' ) @ ( B @ '+' ) ) ),
inference(pattern_uni,[status(thm)],[518:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( G @ ( F @ '==>' ) ))]]) ).
thf(555,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ '==>' ) @ ( C @ '+' ) @ '+' ) )
= ( A @ ( C @ ( B @ '==>' ) @ '+' ) @ ( B @ '+' ) ) ),
inference(simp,[status(thm)],[519]) ).
thf(26970,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ '==>' ) @ '+' ) @ ( C @ '+' ) )
= ( A @ ( C @ ( B @ '==>' ) @ '+' ) @ ( B @ '+' ) ) ),
inference(rewrite,[status(thm)],[555,25]) ).
thf(15,plain,
( ~ sk1
| ( ( b @ ( c @ '==>' ) )
= '0' ) ),
inference(cnfConj,[status(thm)],[12]) ).
thf(22,plain,
( ~ sk1
| ( ( b @ ( c @ '==>' ) )
= '0' ) ),
inference(lifteq,[status(thm)],[15]) ).
thf(172,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| ~ sk1
| ( '0' != '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[22,18]) ).
thf(173,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[172]) ).
thf(184,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= b )
| ( c != c )
| ~ sk1 ),
inference(simp,[status(thm)],[173]) ).
thf(189,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= b )
| ~ sk1 ),
inference(simp,[status(thm)],[184]) ).
thf(602,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[43,581]) ).
thf(657,plain,
! [C: $i,B: $i,A: $i] :
( ( C != b )
| ( ( B @ ( A @ '+' ) )
!= a )
| ( ( c @ ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[602]) ).
thf(692,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ( ( c @ ( b @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[657]) ).
thf(39653,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ( ( c @ ( b @ ( B @ '==>' ) @ ( A @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[692,43]) ).
thf(61,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) ) )
| ~ sk1
| ( '0' != '0' ) ),
inference(paramod_ordered,[status(thm)],[37,18]) ).
thf(62,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[61]) ).
thf(77,plain,
! [A: $i] :
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= '0' )
| ( A != c )
| ~ sk1 ),
inference(simp,[status(thm)],[62]) ).
thf(83,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= '0' )
| ~ sk1 ),
inference(simp,[status(thm)],[77]) ).
thf(405,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) )
!= '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[43,83]) ).
thf(424,plain,
! [C: $i,B: $i,A: $i] :
( ( C != b )
| ( ( B @ ( A @ '+' ) )
!= a )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) )
!= '0' )
| ~ sk1 ),
inference(simp,[status(thm)],[405]) ).
thf(448,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ( ( b @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) )
!= '0' )
| ~ sk1 ),
inference(simp,[status(thm)],[424]) ).
thf(86,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '+' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ( A != c )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[31,79]) ).
thf(91,plain,
( ( ( b @ ( a @ '==>' ) )
!= '0' )
| ( a != c )
| ~ sk1 ),
inference(simp,[status(thm)],[86]) ).
thf(308,plain,
( ( ( b @ ( a @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| ( '0' != '0' )
| ( a != c )
| ~ sk1
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[22,91]) ).
thf(309,plain,
( ( ( b @ ( a @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| ( a != c )
| ~ sk1 ),
inference(simp,[status(thm)],[308]) ).
thf(320,plain,
( ( b != b )
| ( a != c )
| ( a != c )
| ~ sk1 ),
inference(simp,[status(thm)],[309]) ).
thf(321,plain,
( ( a != c )
| ~ sk1 ),
inference(simp,[status(thm)],[320]) ).
thf(416,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) ) )
| sk1
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[43,21]) ).
thf(419,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ( ( B @ ( A @ '+' ) )
!= c )
| sk1
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[416]) ).
thf(443,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= c )
| sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[419]) ).
thf(64169,plain,
! [C: $i,B: $i,A: $i] :
( ( ( b @ ( a @ '==>' ) @ ( c @ '==>' ) )
!= ( C @ ( A @ '==>' ) @ ( B @ '==>' ) ) )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' )
| sk1 ),
inference(paramod_ordered,[status(thm)],[63981,5234]) ).
thf(64170,plain,
( ( ( b @ ( c @ '==>' ) @ ( a @ '==>' ) )
= '0' )
| sk1 ),
inference(pattern_uni,[status(thm)],[64169:[bind(A,$thf( a )),bind(B,$thf( c )),bind(C,$thf( b ))]]) ).
thf(30387,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ( B != b )
| ~ sk1
| ( ( A @ ( B @ '==>' ) )
!= '0' ) ),
inference(paramod_ordered,[status(thm)],[566,189]) ).
thf(30388,plain,
( ( b != b )
| ~ sk1
| ( ( a @ ( b @ '==>' ) )
!= '0' ) ),
inference(pattern_uni,[status(thm)],[30387:[bind(A,$thf( a )),bind(B,$thf( b ))]]) ).
thf(30762,plain,
( ~ sk1
| ( ( a @ ( b @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[30388]) ).
thf(31316,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '==>' ) @ ( B @ '==>' ) )
!= ( a @ ( b @ '==>' ) ) )
| ~ sk1
| ( '0' != '0' ) ),
inference(paramod_ordered,[status(thm)],[8605,30762]) ).
thf(31317,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '==>' ) @ ( B @ '==>' ) )
!= ( a @ ( b @ '==>' ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[31316]) ).
thf(31347,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '==>' ) )
!= a )
| ( B != b )
| ~ sk1 ),
inference(simp,[status(thm)],[31317]) ).
thf(31366,plain,
! [A: $i] :
( ( ( b @ ( A @ '==>' ) )
!= a )
| ~ sk1 ),
inference(simp,[status(thm)],[31347]) ).
thf(64021,plain,
( ( ( b @ ( a @ '==>' ) @ ( c @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| ( '0' != '0' )
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[63981,43485]) ).
thf(64022,plain,
( ( ( b @ ( a @ '==>' ) @ ( c @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| sk1 ),
inference(simp,[status(thm)],[64021]) ).
thf(64455,plain,
( ( ( b @ ( a @ '==>' ) )
!= b )
| ( c != c )
| sk1 ),
inference(simp,[status(thm)],[64022]) ).
thf(64694,plain,
( ( ( b @ ( a @ '==>' ) )
!= b )
| sk1 ),
inference(simp,[status(thm)],[64455]) ).
thf(396,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) ) )
| ~ sk1
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
!= '0' ) ),
inference(paramod_ordered,[status(thm)],[43,18]) ).
thf(428,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ( ( B @ ( A @ '+' ) )
!= c )
| ~ sk1
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[396]) ).
thf(452,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= c )
| ~ sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( B @ '==>' ) @ ( A @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[428]) ).
thf(338,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) )
!= c )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[25,79]) ).
thf(359,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( b @ ( a @ '==>' ) ) )
| ( ( B @ ( A @ '+' ) )
!= a )
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) )
!= c )
| ~ sk1 ),
inference(simp,[status(thm)],[338]) ).
thf(366,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ( ( b @ ( a @ '==>' ) @ ( B @ '+' ) @ ( A @ '+' ) )
!= c )
| ~ sk1 ),
inference(simp,[status(thm)],[359]) ).
thf(100,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| sk1
| ( ( '0' @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[37,21]) ).
thf(123,plain,
! [A: $i] :
( ( b != '0' )
| ( A != a )
| sk1
| ( ( '0' @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[100]) ).
thf(129,plain,
( ( b != '0' )
| sk1
| ( ( '0' @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[123]) ).
thf(4242,plain,
( ( b != '0' )
| sk1
| ( ( a @ ( c @ '==>' ) )
= '0' ) ),
inference(rewrite,[status(thm)],[129,31]) ).
thf(196,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| sk1
| ( '0' != '0' )
| ( ( a @ ( c @ '==>' ) )
!= '0' ) ),
inference(paramod_ordered,[status(thm)],[37,20]) ).
thf(197,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| sk1
| ( ( a @ ( c @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[196]) ).
thf(222,plain,
! [A: $i] :
( ( b != '0' )
| ( A != c )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[197]) ).
thf(237,plain,
( ( b != '0' )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[222]) ).
thf(6119,plain,
( ( ( a @ ( c @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ( b != '0' )
| ( '0' != '0' )
| sk1
| ( b != '0' )
| sk1 ),
inference(paramod_ordered,[status(thm)],[4242,237]) ).
thf(6120,plain,
( ( ( a @ ( c @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ( b != '0' )
| sk1 ),
inference(simp,[status(thm)],[6119]) ).
thf(6121,plain,
( ( b != '0' )
| sk1 ),
inference(pattern_uni,[status(thm)],[6120:[]]) ).
thf(1093,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( '0' != '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[37,951]) ).
thf(1094,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[1093]) ).
thf(1107,plain,
! [A: $i] :
( ( b != '0' )
| ( A != a )
| ~ sk1 ),
inference(simp,[status(thm)],[1094]) ).
thf(1112,plain,
( ( b != '0' )
| ~ sk1 ),
inference(simp,[status(thm)],[1107]) ).
thf(6818,plain,
( ( sk1 != sk1 )
| ( b != '0' )
| ~ $true
| ( b != '0' ) ),
inference(paramod_ordered,[status(thm)],[6121,1112]) ).
thf(6819,plain,
( ( sk1 != sk1 )
| ( b != '0' ) ),
inference(simp,[status(thm)],[6818]) ).
thf(6820,plain,
b != '0',
inference(pattern_uni,[status(thm)],[6819:[]]) ).
thf(478,plain,
! [B: $i,A: $i] :
( ( ( b @ ( c @ '==>' ) )
!= ( B @ ( A @ '==>' ) ) )
| ( ( '0' @ ( A @ '+' ) )
= ( A @ ( B @ '==>' ) @ ( B @ '+' ) ) )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[22,46]) ).
thf(479,plain,
( ( ( c @ ( b @ '==>' ) @ ( b @ '+' ) )
= ( '0' @ ( c @ '+' ) ) )
| ~ sk1 ),
inference(pattern_uni,[status(thm)],[478:[bind(A,$thf( c )),bind(B,$thf( b ))]]) ).
thf(23143,plain,
( ( ( c @ ( b @ '==>' ) @ ( b @ '+' ) )
= c )
| ~ sk1 ),
inference(rewrite,[status(thm)],[479,31]) ).
thf(589,plain,
! [A: $i] :
( ( ( A @ ( '0' @ '+' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) ) )
| ( ( A @ ( a @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[241,581]) ).
thf(663,plain,
! [A: $i] :
( ( A
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) ) )
| ( ( b @ ( a @ '==>' ) )
!= '0' )
| ( ( A @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[589]) ).
thf(699,plain,
( ( ( b @ ( a @ '==>' ) )
!= '0' )
| ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[663]) ).
thf(44035,plain,
( ( ( b @ ( a @ '==>' ) )
!= '0' )
| ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[699,43]) ).
thf(605,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ( ( c @ ( c @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[581,581]) ).
thf(606,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ( ( c @ ( c @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[605]) ).
thf(656,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( a != a )
| ( ( c @ ( c @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[606]) ).
thf(691,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( c @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[656]) ).
thf(38688,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( '0' @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[691,34,43]) ).
thf(388,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[43,34]) ).
thf(389,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ '+' ) @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[388:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ '+' ) )),bind(D,$thf( H @ ( G @ '+' ) ))]]) ).
thf(434,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ '+' ) @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[389]) ).
thf(1413,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ '==>' ) @ ( A @ '+' ) )
!= ( C @ ( B @ '+' ) ) )
| ( ( A @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[1409,434]) ).
thf(1414,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ '==>' ) @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[1413:[bind(A,$thf( E )),bind(B,$thf( E )),bind(C,$thf( E @ ( E @ '==>' ) ))]]) ).
thf(1504,plain,
! [A: $i] :
( ( A @ ( A @ ( A @ '==>' ) @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[1414]) ).
thf(2223,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ '==>' ) @ '==>' ) @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( '0' != '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[1504,951]) ).
thf(2224,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ '==>' ) @ '==>' ) @ ( A @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[2223]) ).
thf(2286,plain,
! [A: $i] :
( ( ( A @ ( A @ ( A @ '==>' ) @ '==>' ) )
!= b )
| ( A != a )
| ~ sk1 ),
inference(simp,[status(thm)],[2224]) ).
thf(2335,plain,
( ( ( a @ ( a @ ( a @ '==>' ) @ '==>' ) )
!= b )
| ~ sk1 ),
inference(simp,[status(thm)],[2286]) ).
thf(11042,plain,
( ( ( a @ ( '0' @ '==>' ) )
!= b )
| ~ sk1 ),
inference(rewrite,[status(thm)],[2335,34]) ).
thf(229,plain,
( ( ( b @ ( c @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[218]) ).
thf(496,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
!= ( D @ ( C @ '+' ) ) )
| ( ( E @ ( A @ ( B @ '==>' ) @ ( B @ '+' ) @ '==>' ) )
= ( E @ ( D @ '==>' ) @ ( C @ '==>' ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,43]) ).
thf(497,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ '==>' ) @ ( C @ '+' ) @ '==>' ) )
= ( A @ ( C @ ( B @ '==>' ) @ '==>' ) @ ( B @ '==>' ) ) ),
inference(pattern_uni,[status(thm)],[496:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( F )),bind(D,$thf( G @ ( F @ '==>' ) ))]]) ).
thf(572,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ '==>' ) @ ( C @ '+' ) @ '==>' ) )
= ( A @ ( C @ ( B @ '==>' ) @ '==>' ) @ ( B @ '==>' ) ) ),
inference(simp,[status(thm)],[497]) ).
thf(32349,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( C @ '==>' ) @ '==>' ) @ ( C @ '==>' ) )
= ( A @ ( C @ ( B @ '==>' ) @ '==>' ) @ ( B @ '==>' ) ) ),
inference(rewrite,[status(thm)],[572,43]) ).
thf(603,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) ) )
| ( ( c @ ( a @ '+' ) )
= c )
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[581,581]) ).
thf(604,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) ) )
| ( ( c @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[603]) ).
thf(679,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) ) )
| ( ( b @ ( a @ '==>' ) )
!= a )
| ( ( c @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[604]) ).
thf(36746,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) ) )
| ( ( b @ ( a @ '==>' ) )
!= a )
| ( ( c @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[679,43]) ).
thf(115,plain,
! [A: $i] :
( ( ( A @ ( '0' @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| sk1
| ( ( A @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[40,21]) ).
thf(117,plain,
! [A: $i] :
( ( A != b )
| ( '0' != a )
| sk1
| ( ( A @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[115]) ).
thf(124,plain,
( ( '0' != a )
| sk1
| ( ( b @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[117]) ).
thf(194,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| sk1
| ( ( b @ ( c @ '==>' ) )
!= '0' )
| ( '0' != '0' ) ),
inference(paramod_ordered,[status(thm)],[37,20]) ).
thf(195,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| sk1
| ( ( b @ ( c @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[194]) ).
thf(227,plain,
! [A: $i] :
( ( '0' != a )
| ( A != c )
| ( ( b @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[195]) ).
thf(233,plain,
( ( '0' != a )
| ( ( b @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[227]) ).
thf(2472,plain,
( ( ( b @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| ( '0' != a )
| ( '0' != '0' )
| sk1
| ( '0' != a )
| sk1 ),
inference(paramod_ordered,[status(thm)],[124,233]) ).
thf(2473,plain,
( ( ( b @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| ( '0' != a )
| sk1 ),
inference(simp,[status(thm)],[2472]) ).
thf(2584,plain,
( ( ( b @ ( a @ '+' ) )
!= b )
| ( c != c )
| ( '0' != a )
| sk1 ),
inference(simp,[status(thm)],[2473]) ).
thf(2619,plain,
( ( ( b @ ( a @ '+' ) )
!= b )
| ( '0' != a )
| sk1 ),
inference(simp,[status(thm)],[2584]) ).
thf(13498,plain,
! [A: $i] :
( ( ( A @ ( '0' @ '+' ) )
!= ( b @ ( a @ '+' ) ) )
| ( A != b )
| ( '0' != a )
| sk1 ),
inference(paramod_ordered,[status(thm)],[241,2619]) ).
thf(13516,plain,
( ( b != b )
| ( '0' != a )
| ( '0' != a )
| sk1 ),
inference(simp,[status(thm)],[13498]) ).
thf(13543,plain,
( ( '0' != a )
| sk1 ),
inference(simp,[status(thm)],[13516]) ).
thf(69,plain,
! [A: $i] :
( ( ( A @ ( '0' @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ~ sk1
| ( ( A @ ( a @ '+' ) @ ( c @ '==>' ) )
!= '0' ) ),
inference(paramod_ordered,[status(thm)],[40,18]) ).
thf(70,plain,
! [A: $i] :
( ( A != b )
| ( '0' != a )
| ~ sk1
| ( ( A @ ( a @ '+' ) @ ( c @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[69]) ).
thf(78,plain,
( ( '0' != a )
| ~ sk1
| ( ( b @ ( a @ '+' ) @ ( c @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[70]) ).
thf(1130,plain,
! [A: $i] :
( ( ( A @ ( '0' @ '+' ) )
!= ( b @ ( a @ '+' ) ) )
| ( '0' != a )
| ~ sk1
| ( ( A @ ( c @ '==>' ) )
!= '0' ) ),
inference(paramod_ordered,[status(thm)],[241,78]) ).
thf(1154,plain,
! [A: $i] :
( ( A != b )
| ( '0' != a )
| ( '0' != a )
| ~ sk1
| ( ( A @ ( c @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[1130]) ).
thf(1161,plain,
( ( '0' != a )
| ~ sk1
| ( ( b @ ( c @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[1154]) ).
thf(9369,plain,
( ( ( b @ ( c @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| ( '0' != a )
| ~ sk1
| ( '0' != '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[22,1161]) ).
thf(9370,plain,
( ( ( b @ ( c @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| ( '0' != a )
| ~ sk1 ),
inference(simp,[status(thm)],[9369]) ).
thf(9371,plain,
( ( '0' != a )
| ~ sk1 ),
inference(pattern_uni,[status(thm)],[9370:[]]) ).
thf(14108,plain,
( ( sk1 != sk1 )
| ( '0' != a )
| ~ $true
| ( '0' != a ) ),
inference(paramod_ordered,[status(thm)],[13543,9371]) ).
thf(14109,plain,
( ( sk1 != sk1 )
| ( '0' != a ) ),
inference(simp,[status(thm)],[14108]) ).
thf(14110,plain,
'0' != a,
inference(pattern_uni,[status(thm)],[14109:[]]) ).
thf(327,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
!= ( D @ ( '0' @ '+' ) ) )
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[25,241]) ).
thf(355,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C != D )
| ( ( B @ ( A @ '+' ) )
!= '0' )
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) )
= D ) ),
inference(simp,[status(thm)],[327]) ).
thf(362,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= '0' )
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) )
= C ) ),
inference(simp,[status(thm)],[355]) ).
thf(9903,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ '==>' ) @ ( A @ '+' ) )
!= ( C @ ( B @ '+' ) ) )
| ( A != '0' )
| ( ( D @ ( C @ '+' ) @ ( B @ '+' ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[1409,362]) ).
thf(9904,plain,
! [B: $i,A: $i] :
( ( B != '0' )
| ( ( A @ ( B @ ( B @ '==>' ) @ '+' ) @ ( B @ '+' ) )
= A ) ),
inference(pattern_uni,[status(thm)],[9903:[bind(A,$thf( F )),bind(B,$thf( F )),bind(C,$thf( F @ ( F @ '==>' ) )),bind(D,$thf( D ))]]) ).
thf(10150,plain,
! [A: $i] :
( ( A @ ( '0' @ ( '0' @ '==>' ) @ '+' ) @ ( '0' @ '+' ) )
= A ),
inference(simp,[status(thm)],[9904]) ).
thf(10766,plain,
! [A: $i] :
( ( A @ ( '0' @ ( '0' @ '==>' ) @ '+' ) )
= A ),
inference(rewrite,[status(thm)],[10150,241]) ).
thf(14867,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( '0' @ ( '0' @ '==>' ) @ '+' ) )
!= ( C @ ( B @ '+' ) ) )
| ( A != c )
| sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[10766,443]) ).
thf(14868,plain,
! [A: $i] :
( ( A != c )
| sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( A @ '==>' ) @ ( '0' @ ( '0' @ '==>' ) @ '==>' ) )
= '0' ) ),
inference(pattern_uni,[status(thm)],[14867:[bind(A,$thf( A )),bind(B,$thf( '0' @ ( '0' @ '==>' ) )),bind(C,$thf( A ))]]) ).
thf(15140,plain,
( sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) @ ( '0' @ ( '0' @ '==>' ) @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[14868]) ).
thf(22077,plain,
( sk1
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ) ),
inference(rewrite,[status(thm)],[15140,34]) ).
thf(546,plain,
! [B: $i,A: $i] :
( ( ( a @ ( c @ '==>' ) )
!= ( B @ ( A @ '==>' ) ) )
| ( ( '0' @ ( A @ '+' ) )
= ( A @ ( B @ '==>' ) @ ( B @ '+' ) ) )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[19,46]) ).
thf(547,plain,
( ( ( c @ ( a @ '==>' ) @ ( a @ '+' ) )
= ( '0' @ ( c @ '+' ) ) )
| ~ sk1 ),
inference(pattern_uni,[status(thm)],[546:[bind(A,$thf( c )),bind(B,$thf( a ))]]) ).
thf(24592,plain,
( ( ( c @ ( a @ '==>' ) @ ( a @ '+' ) )
= c )
| ~ sk1 ),
inference(rewrite,[status(thm)],[547,31]) ).
thf(601,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[43,581]) ).
thf(678,plain,
! [C: $i,B: $i,A: $i] :
( ( C != b )
| ( ( B @ ( A @ '+' ) )
!= a )
| ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[601]) ).
thf(712,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( B @ '==>' ) @ ( A @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[678]) ).
thf(54522,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( B @ '==>' ) @ ( A @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[712,43]) ).
thf(403,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[19,43]) ).
thf(420,plain,
! [C: $i,B: $i,A: $i] :
( ( C != a )
| ( ( B @ ( A @ '+' ) )
!= c )
| ~ sk1
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[403]) ).
thf(444,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= c )
| ~ sk1
| ( ( a @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[420]) ).
thf(619,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) ) )
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[25,581]) ).
thf(655,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) ) )
| ( ( B @ ( A @ '+' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[619]) ).
thf(690,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( B @ '+' ) @ ( A @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[655]) ).
thf(37768,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( B @ '+' ) @ ( A @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[690,43]) ).
thf(393,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[22,43]) ).
thf(421,plain,
! [C: $i,B: $i,A: $i] :
( ( C != b )
| ( ( B @ ( A @ '+' ) )
!= c )
| ~ sk1
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[393]) ).
thf(445,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= c )
| ~ sk1
| ( ( b @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[421]) ).
thf(200,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| sk1
| ( '0' != '0' )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(paramod_ordered,[status(thm)],[21,20]) ).
thf(201,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[200]) ).
thf(221,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= b )
| ( c != c )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[201]) ).
thf(236,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= b )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[221]) ).
thf(627,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ '==>' ) @ ( B @ '+' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) ) )
| ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[46,581]) ).
thf(665,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ '==>' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) ) )
| ( B
!= ( b @ ( a @ '==>' ) ) )
| ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[627]) ).
thf(701,plain,
! [A: $i] :
( ( ( A @ ( b @ ( a @ '==>' ) @ '==>' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) ) )
| ( ( b @ ( a @ '==>' ) @ ( A @ '==>' ) @ ( A @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[665]) ).
thf(45375,plain,
! [A: $i] :
( ( ( A @ ( b @ ( a @ '==>' ) @ '==>' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) ) )
| ( ( b @ ( a @ '==>' ) @ ( A @ '==>' ) @ ( A @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[701,43]) ).
thf(644,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( '0' @ '+' ) @ ( a @ '+' ) )
= c )
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[21,581]) ).
thf(645,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( '0' @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[644]) ).
thf(668,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= b )
| ( a != c )
| ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( '0' @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[645]) ).
thf(34614,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= b )
| ( a != c )
| ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[668,241]) ).
thf(995,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= ( D @ ( C @ '+' ) ) )
| ( ( A @ ( B @ '+' ) @ ( D @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[28,434]) ).
thf(996,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ '+' ) @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[995:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(397,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ~ sk1
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= '0' ) ),
inference(paramod_ordered,[status(thm)],[43,18]) ).
thf(427,plain,
! [C: $i,B: $i,A: $i] :
( ( C != b )
| ( ( B @ ( A @ '+' ) )
!= a )
| ~ sk1
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[397]) ).
thf(451,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ~ sk1
| ( ( b @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[427]) ).
thf(43749,plain,
! [A: $i] :
( ( ( A @ ( '0' @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ( '0' = A )
| sk1 ),
inference(paramod_ordered,[status(thm)],[41912,40]) ).
thf(43841,plain,
! [A: $i] :
( ( A != a )
| ( '0' != c )
| ( '0' = A )
| sk1 ),
inference(simp,[status(thm)],[43749]) ).
thf(43923,plain,
( ( '0' != c )
| ( '0' = a )
| sk1 ),
inference(simp,[status(thm)],[43841]) ).
thf(52206,plain,
( ( '0' != c )
| sk1 ),
inference(simplifyReflect,[status(thm)],[43923,14110]) ).
thf(176,plain,
! [A: $i] :
( ( ( A @ ( '0' @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| ( '0' = A )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[22,40]) ).
thf(185,plain,
! [A: $i] :
( ( A != b )
| ( '0' != c )
| ~ sk1
| ( '0' = A ) ),
inference(simp,[status(thm)],[176]) ).
thf(190,plain,
( ( '0' != c )
| ~ sk1
| ( b = '0' ) ),
inference(simp,[status(thm)],[185]) ).
thf(1117,plain,
( ( b != b )
| ( '0' != '0' )
| ~ sk1
| ( '0' != c )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[190,1112]) ).
thf(1118,plain,
( ( b != b )
| ( '0' != c )
| ~ sk1 ),
inference(simp,[status(thm)],[1117]) ).
thf(1119,plain,
( ( '0' != c )
| ~ sk1 ),
inference(pattern_uni,[status(thm)],[1118:[]]) ).
thf(52234,plain,
( ( sk1 != sk1 )
| ( '0' != c )
| ~ $true
| ( '0' != c ) ),
inference(paramod_ordered,[status(thm)],[52206,1119]) ).
thf(52235,plain,
( ( sk1 != sk1 )
| ( '0' != c ) ),
inference(simp,[status(thm)],[52234]) ).
thf(52236,plain,
'0' != c,
inference(pattern_uni,[status(thm)],[52235:[]]) ).
thf(49218,plain,
! [B: $i,A: $i] :
( ( ( c @ ( a @ '==>' ) @ ( a @ '+' ) )
!= ( B @ ( A @ '==>' ) @ ( A @ '+' ) ) )
| ( ( A @ ( B @ '==>' ) @ ( B @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[43555,46]) ).
thf(49219,plain,
( ( ( a @ ( c @ '==>' ) @ ( c @ '+' ) )
= c )
| sk1 ),
inference(pattern_uni,[status(thm)],[49218:[bind(A,$thf( a )),bind(B,$thf( c ))]]) ).
thf(6185,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ '==>' ) @ ( B @ '==>' ) )
!= ( D @ ( E @ '==>' ) @ ( D @ '==>' ) ) )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[5234,6166]) ).
thf(6186,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[6185:[bind(A,$thf( A )),bind(B,$thf( C )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( A ))]]) ).
thf(6377,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ '==>' ) @ ( A @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[6186]) ).
thf(401,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( '0' @ '==>' ) )
!= ( D @ ( C @ ( B @ '+' ) @ '==>' ) ) )
| ( A
= ( D @ ( C @ '==>' ) @ ( B @ '==>' ) ) ) ),
inference(paramod_ordered,[status(thm)],[40,43]) ).
thf(431,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A != D )
| ( ( C @ ( B @ '+' ) )
!= '0' )
| ( A
= ( D @ ( C @ '==>' ) @ ( B @ '==>' ) ) ) ),
inference(simp,[status(thm)],[401]) ).
thf(455,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= '0' )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
= C ) ),
inference(simp,[status(thm)],[431]) ).
thf(630,plain,
! [B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
!= ( B @ ( A @ '+' ) ) )
| ( ( A @ ( B @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[581,28]) ).
thf(631,plain,
( ( ( a @ ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ '+' ) )
= c )
| sk1 ),
inference(pattern_uni,[status(thm)],[630:[bind(A,$thf( a )),bind(B,$thf( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) ))]]) ).
thf(1176,plain,
( ( ( a @ ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ '+' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[631,25]) ).
thf(10844,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( '0' @ ( '0' @ '==>' ) @ '+' ) )
!= ( C @ ( B @ '+' ) ) )
| ( ( A @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[10766,434]) ).
thf(10845,plain,
! [A: $i] :
( ( A @ ( A @ '==>' ) @ ( '0' @ ( '0' @ '==>' ) @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[10844:[bind(A,$thf( A )),bind(B,$thf( '0' @ ( '0' @ '==>' ) )),bind(C,$thf( A ))]]) ).
thf(2180,plain,
! [B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( B @ '==>' ) ) )
| ( ( B @ ( '0' @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[37,1504]) ).
thf(2181,plain,
( ( '0' @ ( '0' @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[2180:[bind(A,$thf( '0' )),bind(B,$thf( '0' ))]]) ).
thf(2346,plain,
( ( '0' @ ( '0' @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[2181,40]) ).
thf(12695,plain,
! [A: $i] :
( ( A @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[10845,2346]) ).
thf(818,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( '0' @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[21,600]) ).
thf(819,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( '0' @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[818]) ).
thf(863,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= b )
| ( a != c )
| ( ( c @ ( '0' @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[819]) ).
thf(69083,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= b )
| ( a != c )
| ( ( c @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[863,40]) ).
thf(620,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ( ( c @ ( C @ ( B @ '+' ) @ ( A @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[25,581]) ).
thf(667,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( b @ ( a @ '==>' ) ) )
| ( ( B @ ( A @ '+' ) )
!= a )
| ( ( c @ ( C @ ( B @ '+' ) @ ( A @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[620]) ).
thf(703,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ( ( c @ ( b @ ( a @ '==>' ) @ ( B @ '+' ) @ ( A @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[667]) ).
thf(48046,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ( ( c @ ( b @ ( a @ '==>' ) @ ( B @ '+' ) @ '==>' ) @ ( A @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[703,43]) ).
thf(646,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( '0' @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[21,581]) ).
thf(647,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| ( ( c @ ( '0' @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[646]) ).
thf(677,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= b )
| ( a != c )
| ( ( c @ ( '0' @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[647]) ).
thf(35878,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= b )
| ( a != c )
| ( ( c @ ( '0' @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[677,43]) ).
thf(387,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| sk1
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
!= '0' )
| ( ( a @ ( c @ '==>' ) )
!= '0' ) ),
inference(paramod_ordered,[status(thm)],[43,20]) ).
thf(422,plain,
! [C: $i,B: $i,A: $i] :
( ( C != b )
| ( ( B @ ( A @ '+' ) )
!= c )
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) )
!= '0' )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[387]) ).
thf(446,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= c )
| ( ( b @ ( B @ '==>' ) @ ( A @ '==>' ) )
!= '0' )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[422]) ).
thf(494,plain,
! [C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '+' ) )
!= ( C @ ( B @ '==>' ) @ ( B @ '+' ) ) )
| ( A
= ( B @ ( C @ '==>' ) @ ( C @ '+' ) ) ) ),
inference(paramod_ordered,[status(thm)],[31,46]) ).
thf(553,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ '==>' ) )
!= '0' )
| ( A != B )
| ( A
= ( B @ ( C @ '==>' ) @ ( C @ '+' ) ) ) ),
inference(simp,[status(thm)],[494]) ).
thf(571,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '==>' ) )
!= '0' )
| ( ( A @ ( B @ '==>' ) @ ( B @ '+' ) )
= A ) ),
inference(simp,[status(thm)],[553]) ).
thf(629,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ '==>' ) @ ( B @ '+' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) ) )
| ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[46,581]) ).
thf(669,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ '==>' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) ) )
| ( B != a )
| ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[629]) ).
thf(704,plain,
! [A: $i] :
( ( ( A @ ( a @ '==>' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) ) )
| ( ( a @ ( A @ '==>' ) @ ( A @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[669]) ).
thf(49667,plain,
! [A: $i] :
( ( ( A @ ( a @ '==>' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) ) )
| ( ( a @ ( A @ '==>' ) @ ( A @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[704,43]) ).
thf(417,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '==>' ) )
!= ( b @ ( a @ '==>' ) ) )
| sk1
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[43,21]) ).
thf(426,plain,
! [C: $i,B: $i,A: $i] :
( ( C != b )
| ( ( B @ ( A @ '+' ) )
!= a )
| sk1
| ( ( C @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[417]) ).
thf(450,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| sk1
| ( ( b @ ( B @ '==>' ) @ ( A @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
= '0' ) ),
inference(simp,[status(thm)],[426]) ).
thf(814,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) ) )
| ( ( '0' @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[21,600]) ).
thf(815,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) ) )
| ( ( '0' @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[814]) ).
thf(857,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ '==>' ) ) )
| ( a != c )
| ( ( '0' @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[815]) ).
thf(68827,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ '==>' ) ) )
| ( a != c )
| ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[857,31]) ).
thf(1225,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= ( a @ ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ '+' ) ) )
| ( ( A @ ( B @ '+' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[28,1176]) ).
thf(1226,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( a @ '+' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
= c )
| sk1 ),
inference(pattern_uni,[status(thm)],[1225:[bind(A,$thf( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) )),bind(B,$thf( a ))]]) ).
thf(4834,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( a @ '+' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[1226,43]) ).
thf(802,plain,
! [B: $i,A: $i] :
( ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
!= ( B @ ( A @ '+' ) ) )
| ( ( A @ ( B @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[600,28]) ).
thf(803,plain,
( ( ( a @ ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ '+' ) )
= c )
| sk1 ),
inference(pattern_uni,[status(thm)],[802:[bind(A,$thf( a )),bind(B,$thf( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) ))]]) ).
thf(2876,plain,
( ( ( a @ ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ '+' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[803,25]) ).
thf(2933,plain,
! [B: $i,A: $i] :
( ( ( a @ ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ '+' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
!= ( B @ ( A @ '+' ) ) )
| ( ( A @ ( B @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[2876,28]) ).
thf(2934,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ '+' ) @ '+' ) )
= c )
| sk1 ),
inference(pattern_uni,[status(thm)],[2933:[bind(A,$thf( b @ ( a @ '==>' ) )),bind(B,$thf( a @ ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ '+' ) ))]]) ).
thf(5739,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[2934,25]) ).
thf(593,plain,
! [A: $i] :
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
!= ( '0' @ ( A @ '+' ) ) )
| ( c = A )
| sk1 ),
inference(paramod_ordered,[status(thm)],[581,31]) ).
thf(675,plain,
! [A: $i] :
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
!= '0' )
| ( a != A )
| ( c = A )
| sk1 ),
inference(simp,[status(thm)],[593]) ).
thf(710,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
!= '0' )
| ( a = c )
| sk1 ),
inference(simp,[status(thm)],[675]) ).
thf(53410,plain,
( ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) )
!= '0' )
| ( a = c )
| sk1 ),
inference(rewrite,[status(thm)],[710,43]) ).
thf(39327,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[39115,15790]) ).
thf(39328,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[39327:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(39614,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[39328]) ).
thf(37465,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[37260,15790]) ).
thf(37466,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[37465:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(37658,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[37466]) ).
thf(35588,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( D @ ( D @ '==>' ) ) )
| ( ( '0' @ ( B @ '==>' ) @ ( C @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[35388,15790]) ).
thf(35589,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[35588:[bind(A,$thf( '0' )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( '0' ))]]) ).
thf(35753,plain,
! [B: $i,A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( B @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[35589]) ).
thf(64725,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[35753,63282]) ).
thf(64803,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[64725,6371]) ).
thf(64804,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[64803:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(65410,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[64804]) ).
thf(65445,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[65410,40]) ).
thf(68099,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[37658,65445]) ).
thf(68187,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( '0' @ ( A @ '==>' ) )
!= ( B @ ( D @ '==>' ) ) )
| ( ( '0' @ ( C @ '==>' ) @ ( B @ '==>' ) )
= '0' ) ),
inference(paramod_ordered,[status(thm)],[68099,6371]) ).
thf(68188,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(pattern_uni,[status(thm)],[68187:[bind(A,$thf( A )),bind(B,$thf( '0' )),bind(C,$thf( C )),bind(D,$thf( A ))]]) ).
thf(68645,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) @ ( '0' @ '==>' ) )
= '0' ),
inference(simp,[status(thm)],[68188]) ).
thf(70174,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[68645,40]) ).
thf(71996,plain,
! [A: $i] :
( ( '0' @ ( A @ '==>' ) )
= '0' ),
inference(rewrite,[status(thm)],[39614,70174]) ).
thf(616,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) ) )
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[581,25]) ).
thf(680,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) ) )
| ( ( B @ ( A @ '+' ) )
!= a )
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[616]) ).
thf(713,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ( ( c @ ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( B @ '+' ) @ ( A @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[680]) ).
thf(55660,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ( ( c @ ( b @ ( a @ '==>' ) @ '==>' ) @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( B @ '+' ) @ ( A @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[713,43]) ).
thf(342,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
!= ( E @ ( D @ '+' ) ) )
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) )
= ( D @ ( E @ '+' ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,28]) ).
thf(343,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ '+' ) @ ( B @ '+' ) )
= ( C @ ( B @ '+' ) @ ( A @ '+' ) ) ),
inference(pattern_uni,[status(thm)],[342:[bind(A,$thf( F )),bind(B,$thf( G )),bind(C,$thf( C )),bind(D,$thf( G @ ( F @ '+' ) )),bind(E,$thf( C ))]]) ).
thf(373,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ '+' ) @ ( B @ '+' ) )
= ( C @ ( B @ '+' ) @ ( A @ '+' ) ) ),
inference(simp,[status(thm)],[343]) ).
thf(595,plain,
! [A: $i] :
( ( ( '0' @ ( A @ '+' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ( ( c @ ( A @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(paramod_ordered,[status(thm)],[31,581]) ).
thf(686,plain,
! [A: $i] :
( ( ( b @ ( a @ '==>' ) )
!= '0' )
| ( A != a )
| ( ( c @ ( A @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[595]) ).
thf(720,plain,
( ( ( b @ ( a @ '==>' ) )
!= '0' )
| ( ( c @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[686]) ).
thf(516,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
!= ( E @ ( D @ ( C @ '+' ) @ '+' ) ) )
| ( ( A @ ( B @ '==>' ) @ ( B @ '+' ) )
= ( E @ ( D @ '+' ) @ ( C @ '+' ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,25]) ).
thf(517,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ '+' ) @ ( A @ '==>' ) @ ( A @ '+' ) )
= ( A @ ( C @ ( B @ '+' ) @ '==>' ) @ ( C @ '+' ) @ ( B @ '+' ) ) ),
inference(pattern_uni,[status(thm)],[516:[bind(A,$thf( K @ ( J @ '+' ) )),bind(B,$thf( I )),bind(C,$thf( J )),bind(D,$thf( K )),bind(E,$thf( I @ ( K @ ( J @ '+' ) @ '==>' ) ))]]) ).
thf(554,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ '+' ) @ ( A @ '==>' ) @ ( A @ '+' ) )
= ( A @ ( C @ ( B @ '+' ) @ '==>' ) @ ( C @ '+' ) @ ( B @ '+' ) ) ),
inference(simp,[status(thm)],[517]) ).
thf(25417,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ '+' ) @ ( A @ '==>' ) @ ( A @ '+' ) )
= ( A @ ( C @ '==>' ) @ ( B @ '==>' ) @ ( C @ '+' ) @ ( B @ '+' ) ) ),
inference(rewrite,[status(thm)],[554,43]) ).
thf(812,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ '==>' ) ) )
| ( ( '0' @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[21,600]) ).
thf(813,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) @ ( c @ '==>' ) )
!= ( c @ ( b @ ( a @ '==>' ) @ '==>' ) ) )
| ( ( '0' @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[812]) ).
thf(873,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= c )
| ( ( b @ ( a @ '==>' ) )
!= c )
| ( ( '0' @ ( a @ '==>' ) @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(simp,[status(thm)],[813]) ).
thf(70914,plain,
( ( ( b @ ( a @ '==>' ) @ ( a @ '+' ) )
!= c )
| ( ( b @ ( a @ '==>' ) )
!= c )
| ( ( '0' @ ( b @ ( a @ '==>' ) @ '+' ) @ ( a @ '+' ) )
= c )
| sk1 ),
inference(rewrite,[status(thm)],[873,70174]) ).
thf(204,plain,
! [A: $i] :
( ( ( A @ ( A @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| sk1
| ( '0' != '0' )
| ( ( a @ ( c @ '==>' ) )
!= '0' ) ),
inference(paramod_ordered,[status(thm)],[34,20]) ).
thf(205,plain,
! [A: $i] :
( ( ( A @ ( A @ '==>' ) )
!= ( b @ ( c @ '==>' ) ) )
| sk1
| ( ( a @ ( c @ '==>' ) )
!= '0' ) ),
inference(simp,[status(thm)],[204]) ).
thf(225,plain,
! [A: $i] :
( ( A != b )
| ( A != c )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[205]) ).
thf(231,plain,
( ( b != c )
| ( ( a @ ( c @ '==>' ) )
!= '0' )
| sk1 ),
inference(simp,[status(thm)],[225]) ).
thf(43732,plain,
( ( ( a @ ( c @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ( b != c )
| ( '0' != '0' )
| sk1
| sk1 ),
inference(paramod_ordered,[status(thm)],[41912,231]) ).
thf(43733,plain,
( ( ( a @ ( c @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ( b != c )
| sk1 ),
inference(simp,[status(thm)],[43732]) ).
thf(43734,plain,
( ( b != c )
| sk1 ),
inference(pattern_uni,[status(thm)],[43733:[]]) ).
thf(31335,plain,
( ( ( a @ ( b @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ~ sk1
| ( '0' != '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[19,30762]) ).
thf(31336,plain,
( ( ( a @ ( b @ '==>' ) )
!= ( a @ ( c @ '==>' ) ) )
| ~ sk1 ),
inference(simp,[status(thm)],[31335]) ).
thf(31348,plain,
( ( a != a )
| ( b != c )
| ~ sk1 ),
inference(simp,[status(thm)],[31336]) ).
thf(31367,plain,
( ( b != c )
| ~ sk1 ),
inference(simp,[status(thm)],[31348]) ).
thf(44026,plain,
( ( sk1 != sk1 )
| ( b != c )
| ~ $true
| ( b != c ) ),
inference(paramod_ordered,[status(thm)],[43734,31367]) ).
thf(44027,plain,
( ( sk1 != sk1 )
| ( b != c ) ),
inference(simp,[status(thm)],[44026]) ).
thf(44028,plain,
b != c,
inference(pattern_uni,[status(thm)],[44027:[]]) ).
thf(528,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ '==>' ) @ ( A @ '+' ) )
!= ( D @ ( C @ '+' ) ) )
| ( ( A @ ( B @ '==>' ) @ ( B @ '+' ) )
= ( C @ ( D @ '+' ) ) ) ),
inference(paramod_ordered,[status(thm)],[46,28]) ).
thf(529,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ '==>' ) @ '+' ) )
= ( A @ ( B @ '==>' ) @ ( B @ '+' ) ) ),
inference(pattern_uni,[status(thm)],[528:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ '==>' ) ))]]) ).
thf(560,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ '==>' ) @ '+' ) )
= ( A @ ( B @ '==>' ) @ ( B @ '+' ) ) ),
inference(simp,[status(thm)],[529]) ).
thf(339,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ '+' ) @ '+' ) )
!= ( b @ ( a @ '==>' ) @ ( a @ '+' ) ) )
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) )
!= '0' )
| ~ sk1 ),
inference(paramod_ordered,[status(thm)],[25,83]) ).
thf(357,plain,
! [C: $i,B: $i,A: $i] :
( ( C
!= ( b @ ( a @ '==>' ) ) )
| ( ( B @ ( A @ '+' ) )
!= a )
| ( ( C @ ( B @ '+' ) @ ( A @ '+' ) )
!= '0' )
| ~ sk1 ),
inference(simp,[status(thm)],[339]) ).
thf(364,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ '+' ) )
!= a )
| ( ( b @ ( a @ '==>' ) @ ( B @ '+' ) @ ( A @ '+' ) )
!= '0' )
| ~ sk1 ),
inference(simp,[status(thm)],[357]) ).
thf(80223,plain,
$false,
inference(e,[status(thm)],[67061,59383,6405,365,3285,63981,449,7096,13557,4220,43555,57542,25,1409,43485,14136,16240,26970,189,46,39653,448,29,321,443,64170,31366,1526,64694,452,366,6820,6371,23143,44035,21,6178,28,38,38688,11042,229,566,32349,36746,14110,22077,5639,5234,24592,41,54522,30762,444,32,34,22,44,37768,445,236,45375,34614,41785,996,434,362,451,52236,8605,367,49219,6377,455,1176,41912,241,35,12695,7070,69083,18,951,48046,31,600,15790,43,11,35878,446,571,49667,450,581,40,26,158,68827,4834,23,5739,53410,71996,55660,19,373,79,720,25417,70914,44028,83,560,13048,364]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL895+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.11 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.23/10.50 % Computer : n004.cluster.edu
% 0.23/10.50 % Model : x86_64 x86_64
% 0.23/10.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/10.50 % Memory : 8046.5625MB
% 0.23/10.50 % OS : Linux 6.8.0-71-generic
% 0.23/10.50 % CPULimit : 300
% 0.23/10.50 % WCLimit : 300
% 0.23/10.50 % DateTime : Fri Sep 25 23:47:01 UTC 2026
% 0.23/10.51 % CPUTime :
% 0.23/10.51 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.35/11.37 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.82/11.66 % [INFO] Parsing done (280ms).
% 1.82/11.68 % [INFO] Running in sequential loop mode.
% 2.93/12.30 % [INFO] eprover registered as external prover.
% 2.93/12.32 % [INFO] Scanning for conjecture ...
% 3.14/12.45 % [INFO] Found a conjecture (or negated_conjecture) and 8 axioms. Running axiom selection ...
% 3.30/12.50 % [INFO] Axiom selection finished. Selected 8 axioms (removed 0 axioms).
% 3.30/12.54 % [INFO] Problem is first-order (TPTP FOF).
% 3.30/12.55 % [INFO] Type checking passed.
% 3.30/12.56 % [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 ...
% 149.63/44.63 % External prover 'e' found a proof!
% 149.63/44.63 % [INFO] Killing All external provers ...
% 149.63/44.63 % Time passed: 33918ms (effective reasoning time: 32945ms)
% 149.63/44.63 % Solved by 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)>
% 149.63/44.64 % Axioms used in derivation (8): sos_01, sos_05, sos_02, sos_06, sos_03, sos_07, sos_04, sos_08
% 149.63/44.64 % No. of inferences in proof: 614
% 149.63/44.64 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 33918 ms resp. 32945 ms w/o parsing
% 137.60/44.85 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 137.60/44.86 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------