%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GRP696-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:21:46 AM UTC 2026
% Result : Unsatisfiable 255.29s 70.82s
% Output : Refutation 253.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 52
% Number of leaves : 12
% Syntax : Number of formulae : 1169 ( 446 unt; 0 typ; 0 def)
% Number of atoms : 2068 (2067 equ; 0 cnn)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 11539 (1734 ~; 899 |; 0 &;8906 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 10 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 1394 ( 0 ^;1394 !; 0 ?;1394 :)
% Comments :
%------------------------------------------------------------------------------
thf(mult_decl,type,
mult: $i > $i > $i ).
thf(a_decl,type,
a: $i ).
thf(b_decl,type,
b: $i ).
thf(c_decl,type,
c: $i ).
thf(ld_decl,type,
ld: $i > $i > $i ).
thf(rd_decl,type,
rd: $i > $i > $i ).
thf(unit_decl,type,
unit: $i ).
thf(i_decl,type,
i: $i > $i ).
thf(4,axiom,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ rd ) @ mult ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c03) ).
thf(20,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ rd ) @ mult ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(21,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ rd ) @ mult ) )
= A ),
inference(lifteq,[status(thm)],[20]) ).
thf(6,axiom,
! [A: $i] :
( ( unit @ ( A @ mult ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c05) ).
thf(24,plain,
! [A: $i] :
( ( unit @ ( A @ mult ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(25,plain,
! [A: $i] :
( ( unit @ ( A @ mult ) )
= A ),
inference(lifteq,[status(thm)],[24]) ).
thf(658,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( unit @ ( C @ mult ) ) )
| ( A = C ) ),
inference(paramod_ordered,[status(thm)],[21,25]) ).
thf(659,plain,
! [A: $i] :
( ( unit @ ( A @ rd ) )
= A ),
inference(pattern_uni,[status(thm)],[658:[bind(A,$thf( D )),bind(B,$thf( unit )),bind(C,$thf( unit @ ( D @ rd ) ))]]) ).
thf(713,plain,
! [A: $i] :
( ( unit @ ( A @ rd ) )
= A ),
inference(simp,[status(thm)],[659]) ).
thf(8,axiom,
! [B: $i,A: $i] :
( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
= ( B @ i ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c07) ).
thf(28,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
= ( B @ i ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(29,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
= ( B @ i ) ),
inference(lifteq,[status(thm)],[28]) ).
thf(3,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ mult ) @ ( A @ ld ) )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c02) ).
thf(18,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ mult ) @ ( A @ ld ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(19,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ mult ) @ ( A @ ld ) )
= B ),
inference(lifteq,[status(thm)],[18]) ).
thf(899,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( D @ ( C @ mult ) ) )
| ( ( B @ i @ ( C @ ld ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[29,19]) ).
thf(900,plain,
! [B: $i,A: $i] :
( ( A @ i @ ( B @ ld ) )
= ( B @ ( A @ mult ) @ i ) ),
inference(pattern_uni,[status(thm)],[899:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( G )),bind(D,$thf( G @ ( F @ mult ) @ i ))]]) ).
thf(973,plain,
! [B: $i,A: $i] :
( ( A @ i @ ( B @ ld ) )
= ( B @ ( A @ mult ) @ i ) ),
inference(simp,[status(thm)],[900]) ).
thf(642,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( D @ ( C @ mult ) ) )
| ( ( A @ ( C @ ld ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[21,19]) ).
thf(643,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ rd ) @ ld ) )
= B ),
inference(pattern_uni,[status(thm)],[642:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ rd ) )),bind(D,$thf( F ))]]) ).
thf(712,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ rd ) @ ld ) )
= B ),
inference(simp,[status(thm)],[643]) ).
thf(2294,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ i @ ( B @ ld ) )
!= ( C @ ( D @ ( C @ rd ) @ ld ) ) )
| ( ( B @ ( A @ mult ) @ i )
= D ) ),
inference(paramod_ordered,[status(thm)],[973,712]) ).
thf(2295,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ i @ rd ) @ ( B @ mult ) @ i )
= A ),
inference(pattern_uni,[status(thm)],[2294:[bind(A,$thf( G )),bind(B,$thf( F @ ( G @ i @ rd ) )),bind(C,$thf( G @ i )),bind(D,$thf( F ))]]) ).
thf(2316,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ i @ rd ) @ ( B @ mult ) @ i )
= A ),
inference(simp,[status(thm)],[2295]) ).
thf(11,axiom,
! [A: $i] :
( ( A @ ( A @ i @ mult ) )
= unit ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c10) ).
thf(34,plain,
! [A: $i] :
( ( A @ ( A @ i @ mult ) )
= unit ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(35,plain,
! [A: $i] :
( ( A @ ( A @ i @ mult ) )
= unit ),
inference(lifteq,[status(thm)],[34]) ).
thf(520,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( unit @ ( B @ ld ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[35,19]) ).
thf(521,plain,
! [A: $i] :
( ( unit @ ( A @ i @ ld ) )
= A ),
inference(pattern_uni,[status(thm)],[520:[bind(A,$thf( D )),bind(B,$thf( D @ i )),bind(C,$thf( D ))]]) ).
thf(531,plain,
! [A: $i] :
( ( unit @ ( A @ i @ ld ) )
= A ),
inference(simp,[status(thm)],[521]) ).
thf(12,axiom,
! [A: $i] :
( ( A @ i @ ( A @ mult ) )
= unit ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c11) ).
thf(36,plain,
! [A: $i] :
( ( A @ i @ ( A @ mult ) )
= unit ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(37,plain,
! [A: $i] :
( ( A @ i @ ( A @ mult ) )
= unit ),
inference(lifteq,[status(thm)],[36]) ).
thf(522,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( unit @ ( B @ ld ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[37,19]) ).
thf(523,plain,
! [A: $i] :
( ( unit @ ( A @ ld ) )
= ( A @ i ) ),
inference(pattern_uni,[status(thm)],[522:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ i ))]]) ).
thf(532,plain,
! [A: $i] :
( ( unit @ ( A @ ld ) )
= ( A @ i ) ),
inference(simp,[status(thm)],[523]) ).
thf(571,plain,
! [A: $i] :
( ( A @ i @ i )
= A ),
inference(rewrite,[status(thm)],[531,532]) ).
thf(7,axiom,
! [A: $i] :
( ( A @ ( unit @ mult ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c06) ).
thf(26,plain,
! [A: $i] :
( ( A @ ( unit @ mult ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(27,plain,
! [A: $i] :
( ( A @ ( unit @ mult ) )
= A ),
inference(lifteq,[status(thm)],[26]) ).
thf(1,negated_conjecture,
( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
thf(13,plain,
( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(14,plain,
( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ),
inference(polarity_switch,[status(thm)],[13]) ).
thf(15,plain,
( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ),
inference(lifteq,[status(thm)],[14]) ).
thf(63,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,15]) ).
thf(108,plain,
! [A: $i] :
( ( A != a )
| ( ( b @ ( a @ mult ) )
!= unit )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( A != a ) ),
inference(simp,[status(thm)],[63]) ).
thf(174,plain,
( ( ( b @ ( a @ mult ) )
!= unit )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[108]) ).
thf(189,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( b @ ( a @ mult ) )
!= unit )
| ( ( c @ ( A @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,174]) ).
thf(206,plain,
! [A: $i] :
( ( A != a )
| ( ( a @ ( b @ mult ) )
!= unit )
| ( ( b @ ( a @ mult ) )
!= unit )
| ( c != c )
| ( A != a ) ),
inference(simp,[status(thm)],[189]) ).
thf(240,plain,
( ( ( a @ ( b @ mult ) )
!= unit )
| ( ( b @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[206]) ).
thf(268,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( a @ ( b @ mult ) ) )
| ( unit != unit )
| ( ( b @ ( a @ mult ) )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[35,240]) ).
thf(269,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( a @ ( b @ mult ) ) )
| ( ( b @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[268]) ).
thf(273,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ i )
!= b )
| ( ( b @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[269]) ).
thf(285,plain,
( ( ( a @ i )
!= b )
| ( ( b @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[273]) ).
thf(613,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( a @ i )
!= b )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[37,285]) ).
thf(614,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( a @ i )
!= b ) ),
inference(simp,[status(thm)],[613]) ).
thf(618,plain,
! [A: $i] :
( ( ( A @ i )
!= b )
| ( A != a )
| ( ( a @ i )
!= b ) ),
inference(simp,[status(thm)],[614]) ).
thf(630,plain,
( ( a @ i )
!= b ),
inference(simp,[status(thm)],[618]) ).
thf(762,plain,
! [A: $i] :
( ( ( A @ i @ i )
!= ( a @ i ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[571,630]) ).
thf(765,plain,
( ( b @ i )
!= a ),
inference(simp,[status(thm)],[762]) ).
thf(10877,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ rd ) @ ( B @ mult ) @ i )
!= ( b @ i ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[2316,765]) ).
thf(11017,plain,
! [A: $i] :
( ( a @ ( A @ i @ rd ) @ ( A @ mult ) )
!= b ),
inference(simp,[status(thm)],[10877]) ).
thf(11030,plain,
! [A: $i] :
( ( a @ ( A @ i @ rd ) @ ( A @ mult ) )
!= b ),
inference(simp,[status(thm)],[11017]) ).
thf(11705,plain,
! [B: $i,A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( a @ ( B @ i @ rd ) @ ( B @ mult ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[25,11030]) ).
thf(11753,plain,
! [A: $i] :
( ( ( a @ ( A @ i @ rd ) )
!= unit )
| ( b != A ) ),
inference(simp,[status(thm)],[11705]) ).
thf(11780,plain,
( ( a @ ( b @ i @ rd ) )
!= unit ),
inference(simp,[status(thm)],[11753]) ).
thf(11881,plain,
! [A: $i] :
( ( ( unit @ ( A @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[713,11780]) ).
thf(11895,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[11881]) ).
thf(5,axiom,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ mult ) @ rd ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c04) ).
thf(22,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ mult ) @ rd ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(23,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ mult ) @ rd ) )
= A ),
inference(lifteq,[status(thm)],[22]) ).
thf(787,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( C @ ( unit @ rd ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[35,23]) ).
thf(788,plain,
! [A: $i] :
( ( A @ ( unit @ rd ) )
= ( A @ i ) ),
inference(pattern_uni,[status(thm)],[787:[bind(A,$thf( D )),bind(B,$thf( D @ i )),bind(C,$thf( D ))]]) ).
thf(802,plain,
! [A: $i] :
( ( A @ ( unit @ rd ) )
= ( A @ i ) ),
inference(simp,[status(thm)],[788]) ).
thf(13024,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i ) ),
inference(rewrite,[status(thm)],[11895,802]) ).
thf(923,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( C @ ( D @ mult ) ) )
| ( ( A @ i @ ( C @ mult ) )
= ( D @ i ) ) ),
inference(paramod_ordered,[status(thm)],[21,29]) ).
thf(924,plain,
! [B: $i,A: $i] :
( ( A @ i @ ( B @ mult ) )
= ( B @ ( A @ rd ) @ i ) ),
inference(pattern_uni,[status(thm)],[923:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ rd ) ))]]) ).
thf(975,plain,
! [B: $i,A: $i] :
( ( A @ i @ ( B @ mult ) )
= ( B @ ( A @ rd ) @ i ) ),
inference(simp,[status(thm)],[924]) ).
thf(3287,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ ( B @ mult ) )
!= ( C @ i @ ( C @ mult ) ) )
| ( ( B @ ( A @ rd ) @ i )
= unit ) ),
inference(paramod_ordered,[status(thm)],[975,37]) ).
thf(3288,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ i )
= unit ),
inference(pattern_uni,[status(thm)],[3287:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( A ))]]) ).
thf(10904,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ rd ) @ ( B @ mult ) @ i )
!= ( a @ i ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[2316,630]) ).
thf(11004,plain,
! [A: $i] :
( ( b @ ( A @ i @ rd ) @ ( A @ mult ) )
!= a ),
inference(simp,[status(thm)],[10904]) ).
thf(11074,plain,
! [A: $i] :
( ( b @ ( A @ i @ rd ) @ ( A @ mult ) )
!= a ),
inference(simp,[status(thm)],[11004]) ).
thf(24899,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( b @ ( C @ i @ rd ) @ ( C @ mult ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[21,11074]) ).
thf(24944,plain,
! [B: $i,A: $i] :
( ( A
!= ( b @ ( B @ i @ rd ) ) )
| ( ( A @ ( a @ rd ) )
!= B ) ),
inference(simp,[status(thm)],[24899]) ).
thf(24968,plain,
! [A: $i] :
( ( b @ ( A @ ( a @ rd ) @ i @ rd ) )
!= A ),
inference(simp,[status(thm)],[24944]) ).
thf(41841,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ rd ) )
!= ( b @ ( B @ ( a @ rd ) @ i @ rd ) ) )
| ( ( A @ i )
!= B ) ),
inference(paramod_ordered,[status(thm)],[802,24968]) ).
thf(41948,plain,
! [A: $i] :
( ( b != A )
| ( ( A @ i @ ( a @ rd ) @ i )
!= unit ) ),
inference(simp,[status(thm)],[41841]) ).
thf(41963,plain,
( ( b @ i @ ( a @ rd ) @ i )
!= unit ),
inference(simp,[status(thm)],[41948]) ).
thf(42024,plain,
! [A: $i] :
( ( ( A @ ( A @ rd ) @ i )
!= ( b @ i @ ( a @ rd ) @ i ) )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[3288,41963]) ).
thf(42025,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ i )
!= ( b @ i @ ( a @ rd ) @ i ) ),
inference(simp,[status(thm)],[42024]) ).
thf(42071,plain,
! [A: $i] :
( ( A @ ( A @ rd ) )
!= ( b @ i @ ( a @ rd ) ) ),
inference(simp,[status(thm)],[42025]) ).
thf(48105,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( b @ i @ ( a @ rd ) ) )
| ( A
!= ( C @ ( C @ rd ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,42071]) ).
thf(48167,plain,
! [B: $i,A: $i] :
( ( A
!= ( b @ i ) )
| ( ( A @ ( B @ ( B @ rd ) @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[48105]) ).
thf(48230,plain,
! [A: $i] :
( ( b @ i @ ( A @ ( A @ rd ) @ mult ) )
!= a ),
inference(simp,[status(thm)],[48167]) ).
thf(72247,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ ( B @ mult ) )
!= ( b @ i @ ( C @ ( C @ rd ) @ mult ) ) )
| ( ( B @ ( A @ rd ) @ i )
!= a ) ),
inference(paramod_ordered,[status(thm)],[975,48230]) ).
thf(72248,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ ( b @ rd ) @ i )
!= a ),
inference(pattern_uni,[status(thm)],[72247:[bind(A,$thf( b )),bind(B,$thf( E @ ( E @ rd ) )),bind(C,$thf( E ))]]) ).
thf(72333,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ ( b @ rd ) @ i )
!= a ),
inference(simp,[status(thm)],[72248]) ).
thf(42,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( unit @ ( B @ mult ) ) )
| ( unit = B ) ),
inference(paramod_ordered,[status(thm)],[35,25]) ).
thf(43,plain,
( ( unit @ i )
= unit ),
inference(pattern_uni,[status(thm)],[42:[bind(A,$thf( unit )),bind(B,$thf( unit @ i ))]]) ).
thf(524,plain,
! [C: $i,B: $i,A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( A @ ( B @ ld ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[25,19]) ).
thf(525,plain,
! [A: $i] :
( ( A @ ( A @ ld ) )
= unit ),
inference(pattern_uni,[status(thm)],[524:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( unit ))]]) ).
thf(2298,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ i ) )
| ( ( A @ ( C @ ld ) )
= ( C @ ( B @ mult ) @ i ) ) ),
inference(paramod_ordered,[status(thm)],[571,973]) ).
thf(2299,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) )
= ( A @ ( B @ i @ mult ) @ i ) ),
inference(pattern_uni,[status(thm)],[2298:[bind(A,$thf( D )),bind(B,$thf( D @ i ))]]) ).
thf(2318,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) )
= ( A @ ( B @ i @ mult ) @ i ) ),
inference(simp,[status(thm)],[2299]) ).
thf(13737,plain,
! [A: $i] :
( ( A @ ( A @ i @ mult ) @ i )
= unit ),
inference(rewrite,[status(thm)],[525,2318]) ).
thf(14161,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ ( B @ mult ) )
!= ( C @ ( C @ i @ mult ) ) )
| ( ( B @ ( A @ rd ) @ i @ i )
= unit ) ),
inference(paramod_ordered,[status(thm)],[975,13737]) ).
thf(14162,plain,
! [A: $i] :
( ( A @ i @ i @ ( A @ rd ) @ i @ i )
= unit ),
inference(pattern_uni,[status(thm)],[14161:[bind(A,$thf( E )),bind(B,$thf( E @ i @ i )),bind(C,$thf( E @ i ))]]) ).
thf(14287,plain,
! [A: $i] :
( ( A @ i @ i @ ( A @ rd ) @ i @ i )
= unit ),
inference(simp,[status(thm)],[14162]) ).
thf(19879,plain,
! [A: $i] :
( ( A @ i @ i @ ( A @ rd ) )
= unit ),
inference(rewrite,[status(thm)],[14287,571]) ).
thf(19939,plain,
! [A: $i] :
( ( ( unit @ i )
!= ( A @ i ) )
| ( ( unit @ i @ ( A @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[43,19879]) ).
thf(19940,plain,
( ( unit @ i @ ( unit @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[19939:[bind(A,$thf( unit ))]]) ).
thf(20045,plain,
( ( unit @ i @ i )
= unit ),
inference(rewrite,[status(thm)],[19940,802]) ).
thf(10937,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( B @ ( C @ i @ rd ) @ ( C @ mult ) ) )
| ( ( A @ i )
= B ) ),
inference(paramod_ordered,[status(thm)],[27,2316]) ).
thf(10938,plain,
! [A: $i] :
( ( A @ ( unit @ i @ rd ) @ i )
= A ),
inference(pattern_uni,[status(thm)],[10937:[bind(A,$thf( E @ ( unit @ i @ rd ) )),bind(B,$thf( E )),bind(C,$thf( unit ))]]) ).
thf(11047,plain,
! [A: $i] :
( ( A @ ( unit @ i @ rd ) @ i )
= A ),
inference(simp,[status(thm)],[10938]) ).
thf(11079,plain,
! [A: $i] :
( ( A @ ( unit @ rd ) @ i )
= A ),
inference(rewrite,[status(thm)],[11047,43]) ).
thf(19887,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( B @ i ) )
| ( ( A @ i @ ( B @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[11079,19879]) ).
thf(19888,plain,
! [A: $i] :
( ( A @ i @ ( A @ ( unit @ rd ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[19887:[bind(A,$thf( D )),bind(B,$thf( D @ ( unit @ rd ) ))]]) ).
thf(20020,plain,
! [A: $i] :
( ( A @ i @ ( A @ ( unit @ rd ) @ rd ) )
= unit ),
inference(simp,[status(thm)],[19888]) ).
thf(20759,plain,
! [A: $i] :
( ( A @ i @ ( A @ i @ rd ) )
= unit ),
inference(rewrite,[status(thm)],[20020,802]) ).
thf(20848,plain,
! [A: $i] :
( ( ( unit @ i @ i )
!= ( A @ i ) )
| ( ( A @ i @ ( unit @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[20045,20759]) ).
thf(20849,plain,
( ( unit @ i @ i @ ( unit @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[20848:[bind(A,$thf( unit @ i ))]]) ).
thf(20919,plain,
( ( unit @ i @ i @ i )
= unit ),
inference(rewrite,[status(thm)],[20849,802]) ).
thf(21083,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ i @ ( unit @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[20919,20759]) ).
thf(21084,plain,
( ( unit @ i @ i @ i @ ( unit @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[21083:[bind(A,$thf( unit @ i @ i ))]]) ).
thf(21498,plain,
( ( unit @ i @ i @ i @ i )
= unit ),
inference(rewrite,[status(thm)],[21084,802]) ).
thf(21684,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ i @ ( unit @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[21498,20759]) ).
thf(21685,plain,
( ( unit @ i @ i @ i @ i @ ( unit @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[21684:[bind(A,$thf( unit @ i @ i @ i ))]]) ).
thf(22320,plain,
( ( unit @ i @ i @ i @ i @ i )
= unit ),
inference(rewrite,[status(thm)],[21685,802]) ).
thf(22535,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ i @ ( unit @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[22320,20759]) ).
thf(22536,plain,
( ( unit @ i @ i @ i @ i @ i @ ( unit @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[22535:[bind(A,$thf( unit @ i @ i @ i @ i ))]]) ).
thf(22781,plain,
( ( unit @ i @ i @ i @ i @ i @ i )
= unit ),
inference(rewrite,[status(thm)],[22536,802]) ).
thf(23026,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ i @ ( unit @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[22781,20759]) ).
thf(23027,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ ( unit @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[23026:[bind(A,$thf( unit @ i @ i @ i @ i @ i ))]]) ).
thf(23685,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i )
= unit ),
inference(rewrite,[status(thm)],[23027,802]) ).
thf(23967,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ i @ ( unit @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[23685,20759]) ).
thf(23968,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ ( unit @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[23967:[bind(A,$thf( unit @ i @ i @ i @ i @ i @ i ))]]) ).
thf(24324,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i )
= unit ),
inference(rewrite,[status(thm)],[23968,802]) ).
thf(24642,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ i @ ( unit @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[24324,20759]) ).
thf(24643,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ ( unit @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[24642:[bind(A,$thf( unit @ i @ i @ i @ i @ i @ i @ i ))]]) ).
thf(25423,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i )
= unit ),
inference(rewrite,[status(thm)],[24643,802]) ).
thf(25786,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ i @ ( unit @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[25423,20759]) ).
thf(25787,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ ( unit @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[25786:[bind(A,$thf( unit @ i @ i @ i @ i @ i @ i @ i @ i ))]]) ).
thf(28857,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i )
= unit ),
inference(rewrite,[status(thm)],[25787,802]) ).
thf(29280,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ i @ ( unit @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[28857,20759]) ).
thf(29281,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ ( unit @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[29280:[bind(A,$thf( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i ))]]) ).
thf(34257,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i )
= unit ),
inference(rewrite,[status(thm)],[29281,802]) ).
thf(34758,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ i @ ( unit @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[34257,20759]) ).
thf(34759,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ ( unit @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[34758:[bind(A,$thf( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i ))]]) ).
thf(42257,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i )
= unit ),
inference(rewrite,[status(thm)],[34759,802]) ).
thf(42850,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ i @ ( unit @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[42257,20759]) ).
thf(42851,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ ( unit @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[42850:[bind(A,$thf( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i ))]]) ).
thf(79445,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i )
= unit ),
inference(rewrite,[status(thm)],[42851,802]) ).
thf(11711,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( a @ ( C @ i @ rd ) @ ( C @ mult ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[21,11030]) ).
thf(11759,plain,
! [B: $i,A: $i] :
( ( A
!= ( a @ ( B @ i @ rd ) ) )
| ( ( A @ ( b @ rd ) )
!= B ) ),
inference(simp,[status(thm)],[11711]) ).
thf(11786,plain,
! [A: $i] :
( ( a @ ( A @ ( b @ rd ) @ i @ rd ) )
!= A ),
inference(simp,[status(thm)],[11759]) ).
thf(32696,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ i @ ( A @ rd ) )
!= ( a @ ( B @ ( b @ rd ) @ i @ rd ) ) )
| ( unit != B ) ),
inference(paramod_ordered,[status(thm)],[19879,11786]) ).
thf(32768,plain,
! [A: $i] :
( ( ( A @ i @ i )
!= a )
| ( A
!= ( unit @ ( b @ rd ) @ i ) ) ),
inference(simp,[status(thm)],[32696]) ).
thf(32793,plain,
( ( unit @ ( b @ rd ) @ i @ i @ i )
!= a ),
inference(simp,[status(thm)],[32768]) ).
thf(34088,plain,
( ( unit @ ( b @ rd ) @ i )
!= a ),
inference(rewrite,[status(thm)],[32793,571]) ).
thf(76356,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ ( B @ rd ) @ ( b @ rd ) @ i ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[571,72333]) ).
thf(76374,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ ( b @ rd ) )
!= ( a @ i ) ),
inference(simp,[status(thm)],[76356]) ).
thf(76417,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ ( b @ rd ) )
!= ( a @ i ) ),
inference(simp,[status(thm)],[76374]) ).
thf(2,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) @ ( A @ mult ) )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c01) ).
thf(16,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) @ ( A @ mult ) )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(17,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) @ ( A @ mult ) )
= B ),
inference(lifteq,[status(thm)],[16]) ).
thf(309,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) )
| ( B
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,15]) ).
thf(353,plain,
! [A: $i] :
( ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) @ ( A @ ld ) )
!= ( c @ ( a @ mult ) ) )
| ( A
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[309]) ).
thf(390,plain,
( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ ld ) )
!= ( c @ ( a @ mult ) ) ),
inference(simp,[status(thm)],[353]) ).
thf(43763,plain,
( ( a @ ( b @ ( a @ mult ) @ mult ) @ ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) @ i @ mult ) @ i )
!= ( c @ ( a @ mult ) ) ),
inference(rewrite,[status(thm)],[390,2318]) ).
thf(32721,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( a @ ( C @ ( b @ rd ) @ i @ rd ) ) )
| ( A != C ) ),
inference(paramod_ordered,[status(thm)],[23,11786]) ).
thf(32774,plain,
! [B: $i,A: $i] :
( ( A != a )
| ( ( A @ ( B @ mult ) )
!= ( B @ ( b @ rd ) @ i ) ) ),
inference(simp,[status(thm)],[32721]) ).
thf(32795,plain,
! [A: $i] :
( ( a @ ( A @ mult ) )
!= ( A @ ( b @ rd ) @ i ) ),
inference(simp,[status(thm)],[32774]) ).
thf(46863,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( a @ ( C @ mult ) ) )
| ( ( B @ i )
!= ( C @ ( b @ rd ) @ i ) ) ),
inference(paramod_ordered,[status(thm)],[29,32795]) ).
thf(46919,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= a )
| ( A != C )
| ( B
!= ( C @ ( b @ rd ) ) ) ),
inference(simp,[status(thm)],[46863]) ).
thf(46959,plain,
! [A: $i] :
( ( A @ ( A @ ( b @ rd ) @ mult ) @ i )
!= a ),
inference(simp,[status(thm)],[46919]) ).
thf(68375,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ ( B @ ( b @ rd ) @ mult ) @ i ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[571,46959]) ).
thf(68428,plain,
! [A: $i] :
( ( A @ ( A @ ( b @ rd ) @ mult ) )
!= ( a @ i ) ),
inference(simp,[status(thm)],[68375]) ).
thf(68461,plain,
! [A: $i] :
( ( A @ ( A @ ( b @ rd ) @ mult ) )
!= ( a @ i ) ),
inference(simp,[status(thm)],[68428]) ).
thf(74290,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( C @ ( C @ ( b @ rd ) @ mult ) ) )
| ( ( B @ i )
!= ( a @ i ) ) ),
inference(paramod_ordered,[status(thm)],[29,68461]) ).
thf(74324,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= C )
| ( A
!= ( C @ ( b @ rd ) ) )
| ( B != a ) ),
inference(simp,[status(thm)],[74290]) ).
thf(74356,plain,
! [A: $i] :
( ( A @ ( b @ rd ) @ ( a @ mult ) @ i )
!= A ),
inference(simp,[status(thm)],[74324]) ).
thf(76447,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( C @ ( b @ rd ) @ ( a @ mult ) ) )
| ( ( A @ i )
!= C ) ),
inference(paramod_ordered,[status(thm)],[21,74356]) ).
thf(76545,plain,
! [B: $i,A: $i] :
( ( B
!= ( A @ i @ ( b @ rd ) ) )
| ( ( B @ ( A @ rd ) )
!= a ) ),
inference(simp,[status(thm)],[76447]) ).
thf(76588,plain,
! [A: $i] :
( ( A @ i @ ( b @ rd ) @ ( A @ rd ) )
!= a ),
inference(simp,[status(thm)],[76545]) ).
thf(86304,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( C @ i @ ( b @ rd ) @ ( C @ rd ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[23,76588]) ).
thf(86337,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ i @ ( b @ rd ) ) )
| ( ( A @ ( a @ mult ) )
!= B ) ),
inference(simp,[status(thm)],[86304]) ).
thf(86361,plain,
! [A: $i] :
( ( A @ ( a @ mult ) @ i @ ( b @ rd ) )
!= A ),
inference(simp,[status(thm)],[86337]) ).
thf(11870,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( ( A @ i )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[802,11780]) ).
thf(11889,plain,
! [A: $i] :
( ( A != a )
| ( ( b @ i )
!= unit )
| ( ( A @ i )
!= unit ) ),
inference(simp,[status(thm)],[11870]) ).
thf(11917,plain,
( ( ( b @ i )
!= unit )
| ( ( a @ i )
!= unit ) ),
inference(simp,[status(thm)],[11889]) ).
thf(12849,plain,
( ( unit != unit )
| ( ( b @ i )
!= ( a @ i ) )
| ( ( a @ i )
!= unit ) ),
inference(eqfactor_ordered,[status(thm)],[11917]) ).
thf(12855,plain,
( ( ( b @ i )
!= ( a @ i ) )
| ( ( a @ i )
!= unit ) ),
inference(simp,[status(thm)],[12849]) ).
thf(14765,plain,
( ( ( unit @ i )
!= ( a @ i ) )
| ( ( b @ i )
!= ( a @ i ) )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[43,12855]) ).
thf(14766,plain,
( ( ( unit @ i )
!= ( a @ i ) )
| ( ( b @ i )
!= ( a @ i ) ) ),
inference(simp,[status(thm)],[14765]) ).
thf(14805,plain,
( ( unit != a )
| ( ( b @ i )
!= ( a @ i ) ) ),
inference(simp,[status(thm)],[14766]) ).
thf(14839,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( b @ i ) )
| ( unit != a )
| ( A
!= ( a @ i ) ) ),
inference(paramod_ordered,[status(thm)],[11079,14805]) ).
thf(14855,plain,
( ( ( a @ i @ ( unit @ rd ) )
!= b )
| ( unit != a ) ),
inference(simp,[status(thm)],[14839]) ).
thf(16830,plain,
( ( ( a @ i @ i )
!= b )
| ( unit != a ) ),
inference(rewrite,[status(thm)],[14855,802]) ).
thf(32691,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ rd ) )
!= ( a @ ( B @ ( b @ rd ) @ i @ rd ) ) )
| ( ( A @ i )
!= B ) ),
inference(paramod_ordered,[status(thm)],[802,11786]) ).
thf(32736,plain,
! [A: $i] :
( ( a != A )
| ( ( A @ i @ ( b @ rd ) @ i )
!= unit ) ),
inference(simp,[status(thm)],[32691]) ).
thf(32802,plain,
( ( a @ i @ ( b @ rd ) @ i )
!= unit ),
inference(simp,[status(thm)],[32736]) ).
thf(32704,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ rd ) @ i )
!= ( C @ ( b @ rd ) @ i ) )
| ( ( a @ ( A @ i @ ( B @ mult ) @ rd ) )
!= C ) ),
inference(paramod_ordered,[status(thm)],[975,11786]) ).
thf(32705,plain,
! [A: $i] :
( ( a @ ( b @ i @ ( A @ mult ) @ rd ) )
!= A ),
inference(pattern_uni,[status(thm)],[32704:[bind(A,$thf( b )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(32800,plain,
! [A: $i] :
( ( a @ ( b @ i @ ( A @ mult ) @ rd ) )
!= A ),
inference(simp,[status(thm)],[32705]) ).
thf(635,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( C @ ( unit @ mult ) ) )
| ( A = C ) ),
inference(paramod_ordered,[status(thm)],[21,27]) ).
thf(691,plain,
! [C: $i,B: $i,A: $i] :
( ( B != C )
| ( ( B @ ( A @ rd ) )
!= unit )
| ( A = C ) ),
inference(simp,[status(thm)],[635]) ).
thf(741,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ rd ) )
!= unit )
| ( A = B ) ),
inference(simp,[status(thm)],[691]) ).
thf(779,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( D @ ( C @ mult ) ) )
| ( ( D @ ( B @ rd ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[17,23]) ).
thf(780,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) @ ( B @ rd ) )
= A ),
inference(pattern_uni,[status(thm)],[779:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ ld ) ))]]) ).
thf(804,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ld ) @ ( B @ rd ) )
= A ),
inference(simp,[status(thm)],[780]) ).
thf(13036,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( B @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A
!= ( unit @ i ) ) ),
inference(paramod_ordered,[status(thm)],[804,13024]) ).
thf(13056,plain,
! [A: $i] :
( ( ( A @ ( unit @ i @ ld ) )
!= a )
| ( A
!= ( b @ i ) ) ),
inference(simp,[status(thm)],[13036]) ).
thf(13070,plain,
( ( b @ i @ ( unit @ i @ ld ) )
!= a ),
inference(simp,[status(thm)],[13056]) ).
thf(13082,plain,
( ( unit @ i @ ( b @ mult ) @ i )
!= a ),
inference(rewrite,[status(thm)],[13070,973]) ).
thf(13109,plain,
! [A: $i] :
( ( ( A @ i @ i )
!= ( unit @ i @ ( b @ mult ) @ i ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[571,13082]) ).
thf(13140,plain,
( ( unit @ i @ ( b @ mult ) )
!= ( a @ i ) ),
inference(simp,[status(thm)],[13109]) ).
thf(13743,plain,
( ( unit @ ( b @ mult ) )
!= ( a @ i ) ),
inference(rewrite,[status(thm)],[13140,43]) ).
thf(13744,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( unit @ ( b @ mult ) ) )
| ( ( B @ i )
!= ( a @ i ) ) ),
inference(paramod_ordered,[status(thm)],[29,13743]) ).
thf(13760,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= unit )
| ( A != b )
| ( B != a ) ),
inference(simp,[status(thm)],[13744]) ).
thf(13773,plain,
( ( b @ ( a @ mult ) @ i )
!= unit ),
inference(simp,[status(thm)],[13760]) ).
thf(13803,plain,
! [A: $i] :
( ( ( A @ ( A @ rd ) @ i )
!= ( b @ ( a @ mult ) @ i ) )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[3288,13773]) ).
thf(13804,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ i )
!= ( b @ ( a @ mult ) @ i ) ),
inference(simp,[status(thm)],[13803]) ).
thf(13811,plain,
! [A: $i] :
( ( A @ ( A @ rd ) )
!= ( b @ ( a @ mult ) ) ),
inference(simp,[status(thm)],[13804]) ).
thf(272,plain,
( ( unit != unit )
| ( ( a @ ( b @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( b @ ( a @ mult ) )
!= unit ) ),
inference(eqfactor_ordered,[status(thm)],[240]) ).
thf(284,plain,
( ( b != a )
| ( b != a )
| ( ( b @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[272]) ).
thf(287,plain,
( ( b != a )
| ( ( b @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[284]) ).
thf(306,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( b != a )
| ( B != unit ) ),
inference(paramod_ordered,[status(thm)],[17,287]) ).
thf(361,plain,
! [A: $i] :
( ( ( unit @ ( A @ ld ) @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( b != a ) ),
inference(simp,[status(thm)],[306]) ).
thf(32356,plain,
! [A: $i] :
( ( ( A @ ( unit @ i @ mult ) @ i @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( b != a ) ),
inference(rewrite,[status(thm)],[361,2318]) ).
thf(41857,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ rd ) @ i )
!= ( C @ ( a @ rd ) @ i ) )
| ( ( b @ ( A @ i @ ( B @ mult ) @ rd ) )
!= C ) ),
inference(paramod_ordered,[status(thm)],[975,24968]) ).
thf(41858,plain,
! [A: $i] :
( ( b @ ( a @ i @ ( A @ mult ) @ rd ) )
!= A ),
inference(pattern_uni,[status(thm)],[41857:[bind(A,$thf( a )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(41953,plain,
! [A: $i] :
( ( b @ ( a @ i @ ( A @ mult ) @ rd ) )
!= A ),
inference(simp,[status(thm)],[41858]) ).
thf(917,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( unit @ ( C @ mult ) ) )
| ( ( B @ i )
= C ) ),
inference(paramod_ordered,[status(thm)],[29,25]) ).
thf(928,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= unit )
| ( A != C )
| ( ( B @ i )
= C ) ),
inference(simp,[status(thm)],[917]) ).
thf(977,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ mult ) @ i )
!= unit )
| ( ( A @ i )
= B ) ),
inference(simp,[status(thm)],[928]) ).
thf(66,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( A @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,15]) ).
thf(104,plain,
! [A: $i] :
( ( A != c )
| ( unit != a )
| ( ( A @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[66]) ).
thf(170,plain,
( ( unit != a )
| ( ( c @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[104]) ).
thf(24928,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ i ) )
| ( ( b @ ( A @ rd ) @ ( B @ mult ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[571,11074]) ).
thf(24929,plain,
! [A: $i] :
( ( b @ ( A @ rd ) @ ( A @ i @ mult ) )
!= a ),
inference(pattern_uni,[status(thm)],[24928:[bind(A,$thf( C )),bind(B,$thf( C @ i ))]]) ).
thf(24962,plain,
! [A: $i] :
( ( b @ ( A @ rd ) @ ( A @ i @ mult ) )
!= a ),
inference(simp,[status(thm)],[24929]) ).
thf(40351,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( b @ ( A @ rd ) @ ( unit @ mult ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[21498,24962]) ).
thf(40352,plain,
( ( b @ ( unit @ i @ i @ i @ rd ) @ ( unit @ mult ) )
!= a ),
inference(pattern_uni,[status(thm)],[40351:[bind(A,$thf( unit @ i @ i @ i ))]]) ).
thf(40568,plain,
( ( b @ ( unit @ i @ i @ i @ rd ) )
!= a ),
inference(rewrite,[status(thm)],[40352,27]) ).
thf(13101,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ ( B @ mult ) )
!= ( unit @ i @ ( b @ mult ) ) )
| ( ( B @ ( A @ rd ) @ i @ i )
!= a ) ),
inference(paramod_ordered,[status(thm)],[975,13082]) ).
thf(13102,plain,
( ( b @ ( unit @ rd ) @ i @ i )
!= a ),
inference(pattern_uni,[status(thm)],[13101:[bind(A,$thf( unit )),bind(B,$thf( b ))]]) ).
thf(13647,plain,
( ( b @ ( unit @ rd ) )
!= a ),
inference(rewrite,[status(thm)],[13102,571]) ).
thf(13655,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( b @ ( unit @ rd ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[23,13647]) ).
thf(13660,plain,
! [A: $i] :
( ( A != b )
| ( ( A @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[13655]) ).
thf(13675,plain,
( ( b @ ( a @ mult ) )
!= unit ),
inference(simp,[status(thm)],[13660]) ).
thf(3601,plain,
! [A: $i] :
( ( ( A @ ( A @ rd ) @ i )
!= ( b @ i ) )
| ( unit != a ) ),
inference(paramod_ordered,[status(thm)],[3288,765]) ).
thf(3649,plain,
! [A: $i] :
( ( ( A @ ( A @ rd ) )
!= b )
| ( unit != a ) ),
inference(simp,[status(thm)],[3601]) ).
thf(19932,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ i @ mult ) @ i )
!= ( B @ i ) )
| ( ( unit @ i @ ( B @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[13737,19879]) ).
thf(19933,plain,
! [A: $i] :
( ( unit @ i @ ( A @ ( A @ i @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[19932:[bind(A,$thf( D )),bind(B,$thf( D @ ( D @ i @ mult ) ))]]) ).
thf(20029,plain,
! [A: $i] :
( ( unit @ i @ ( A @ ( A @ i @ mult ) @ rd ) )
= unit ),
inference(simp,[status(thm)],[19933]) ).
thf(48409,plain,
! [A: $i] :
( ( unit @ ( A @ ( A @ i @ mult ) @ rd ) )
= unit ),
inference(rewrite,[status(thm)],[20029,43]) ).
thf(14754,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( b @ i ) )
| ( A
!= ( a @ i ) )
| ( ( a @ i )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[11079,12855]) ).
thf(14774,plain,
( ( ( a @ i @ ( unit @ rd ) )
!= b )
| ( ( a @ i )
!= unit ) ),
inference(simp,[status(thm)],[14754]) ).
thf(19242,plain,
( ( ( a @ i @ i )
!= b )
| ( ( a @ i )
!= unit ) ),
inference(rewrite,[status(thm)],[14774,802]) ).
thf(645,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( A @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,15]) ).
thf(663,plain,
! [B: $i,A: $i] :
( ( B != b )
| ( ( B @ ( A @ rd ) )
!= a )
| ( ( c @ ( a @ mult ) @ ( a @ ( A @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[645]) ).
thf(715,plain,
! [A: $i] :
( ( ( b @ ( A @ rd ) )
!= a )
| ( ( c @ ( a @ mult ) @ ( a @ ( A @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[663]) ).
thf(48544,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i )
!= ( A @ i ) )
| ( ( unit @ ( A @ ( unit @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[20919,48409]) ).
thf(48545,plain,
( ( unit @ ( unit @ i @ i @ ( unit @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48544:[bind(A,$thf( unit @ i @ i ))]]) ).
thf(51851,plain,
( ( unit @ i @ i @ ( unit @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48545,713]) ).
thf(41874,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( b @ ( C @ ( a @ rd ) @ i @ rd ) ) )
| ( A != C ) ),
inference(paramod_ordered,[status(thm)],[23,24968]) ).
thf(41884,plain,
! [B: $i,A: $i] :
( ( A != b )
| ( ( A @ ( B @ mult ) )
!= ( B @ ( a @ rd ) @ i ) ) ),
inference(simp,[status(thm)],[41874]) ).
thf(41955,plain,
! [A: $i] :
( ( b @ ( A @ mult ) )
!= ( A @ ( a @ rd ) @ i ) ),
inference(simp,[status(thm)],[41884]) ).
thf(47944,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( b @ ( C @ mult ) ) )
| ( ( B @ i )
!= ( C @ ( a @ rd ) @ i ) ) ),
inference(paramod_ordered,[status(thm)],[29,41955]) ).
thf(48002,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= b )
| ( A != C )
| ( B
!= ( C @ ( a @ rd ) ) ) ),
inference(simp,[status(thm)],[47944]) ).
thf(48031,plain,
! [A: $i] :
( ( A @ ( A @ ( a @ rd ) @ mult ) @ i )
!= b ),
inference(simp,[status(thm)],[48002]) ).
thf(71482,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ ( B @ ( a @ rd ) @ mult ) @ i ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[571,48031]) ).
thf(71508,plain,
! [A: $i] :
( ( A @ ( A @ ( a @ rd ) @ mult ) )
!= ( b @ i ) ),
inference(simp,[status(thm)],[71482]) ).
thf(71555,plain,
! [A: $i] :
( ( A @ ( A @ ( a @ rd ) @ mult ) )
!= ( b @ i ) ),
inference(simp,[status(thm)],[71508]) ).
thf(76045,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( C @ ( C @ ( a @ rd ) @ mult ) ) )
| ( ( B @ i )
!= ( b @ i ) ) ),
inference(paramod_ordered,[status(thm)],[29,71555]) ).
thf(76102,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= C )
| ( A
!= ( C @ ( a @ rd ) ) )
| ( B != b ) ),
inference(simp,[status(thm)],[76045]) ).
thf(76114,plain,
! [A: $i] :
( ( A @ ( a @ rd ) @ ( b @ mult ) @ i )
!= A ),
inference(simp,[status(thm)],[76102]) ).
thf(84958,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ ( a @ rd ) @ ( b @ mult ) @ i ) )
| ( A != B ) ),
inference(paramod_ordered,[status(thm)],[571,76114]) ).
thf(84993,plain,
! [A: $i] :
( ( A @ ( a @ rd ) @ ( b @ mult ) )
!= ( A @ i ) ),
inference(simp,[status(thm)],[84958]) ).
thf(85072,plain,
! [A: $i] :
( ( A @ ( a @ rd ) @ ( b @ mult ) )
!= ( A @ i ) ),
inference(simp,[status(thm)],[84993]) ).
thf(905,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( a @ ( b @ mult ) ) )
| ( ( c @ ( a @ ( B @ i @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,15]) ).
thf(958,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= a )
| ( A != b )
| ( ( c @ ( a @ ( B @ i @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[905]) ).
thf(1001,plain,
! [A: $i] :
( ( ( b @ ( A @ mult ) @ i )
!= a )
| ( ( c @ ( a @ ( A @ i @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[958]) ).
thf(781,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( C @ ( A @ rd ) )
= B ) ),
inference(paramod_ordered,[status(thm)],[27,23]) ).
thf(782,plain,
! [A: $i] :
( ( A @ ( A @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[781:[bind(A,$thf( A )),bind(B,$thf( unit )),bind(C,$thf( A ))]]) ).
thf(14169,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) @ i )
!= ( b @ ( a @ mult ) @ i ) )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[13737,13773]) ).
thf(14170,plain,
! [A: $i] :
( ( A @ ( A @ i @ mult ) @ i )
!= ( b @ ( a @ mult ) @ i ) ),
inference(simp,[status(thm)],[14169]) ).
thf(14259,plain,
! [A: $i] :
( ( A @ ( A @ i @ mult ) )
!= ( b @ ( a @ mult ) ) ),
inference(simp,[status(thm)],[14170]) ).
thf(38062,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ ( unit @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[22320,14259]) ).
thf(38063,plain,
( ( unit @ i @ i @ i @ i @ ( unit @ mult ) )
!= ( b @ ( a @ mult ) ) ),
inference(pattern_uni,[status(thm)],[38062:[bind(A,$thf( unit @ i @ i @ i @ i ))]]) ).
thf(39557,plain,
( ( b @ ( a @ mult ) )
!= ( unit @ i @ i @ i @ i ) ),
inference(rewrite,[status(thm)],[38063,27]) ).
thf(896,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( D @ ( C @ mult ) ) )
| ( ( D @ ( B @ i @ rd ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[29,23]) ).
thf(897,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ mult ) @ i @ ( A @ i @ rd ) )
= B ),
inference(pattern_uni,[status(thm)],[896:[bind(A,$thf( G )),bind(B,$thf( F )),bind(C,$thf( G )),bind(D,$thf( G @ ( F @ mult ) @ i ))]]) ).
thf(972,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ mult ) @ i @ ( A @ i @ rd ) )
= B ),
inference(simp,[status(thm)],[897]) ).
thf(1785,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ i ) )
| ( ( C @ ( B @ mult ) @ i @ ( A @ rd ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[571,972]) ).
thf(1786,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
= A ),
inference(pattern_uni,[status(thm)],[1785:[bind(A,$thf( D )),bind(B,$thf( D @ i ))]]) ).
thf(1825,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
= A ),
inference(simp,[status(thm)],[1786]) ).
thf(1756,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( A @ i @ ( B @ i @ rd ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[27,972]) ).
thf(1757,plain,
! [A: $i] :
( ( A @ i @ ( unit @ i @ rd ) )
= A ),
inference(pattern_uni,[status(thm)],[1756:[bind(A,$thf( A )),bind(B,$thf( unit )),bind(C,$thf( A ))]]) ).
thf(1829,plain,
! [A: $i] :
( ( A @ i @ ( unit @ rd ) )
= A ),
inference(rewrite,[status(thm)],[1757,43]) ).
thf(24921,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i )
!= ( A @ i ) )
| ( ( b @ ( unit @ rd ) @ ( A @ mult ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[20919,11074]) ).
thf(24922,plain,
( ( b @ ( unit @ rd ) @ ( unit @ i @ i @ mult ) )
!= a ),
inference(pattern_uni,[status(thm)],[24921:[bind(A,$thf( unit @ i @ i ))]]) ).
thf(25060,plain,
( ( b @ i @ ( unit @ mult ) )
!= a ),
inference(rewrite,[status(thm)],[24922,802,20045]) ).
thf(25070,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( b @ i @ ( unit @ mult ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[21,25060]) ).
thf(25099,plain,
! [A: $i] :
( ( A
!= ( b @ i ) )
| ( ( A @ ( a @ rd ) )
!= unit ) ),
inference(simp,[status(thm)],[25070]) ).
thf(25119,plain,
( ( b @ i @ ( a @ rd ) )
!= unit ),
inference(simp,[status(thm)],[25099]) ).
thf(25152,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( b @ i @ ( a @ rd ) ) )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[1829,25119]) ).
thf(25173,plain,
( ( unit @ i @ ( unit @ rd ) )
!= ( b @ i @ ( a @ rd ) ) ),
inference(simp,[status(thm)],[25152]) ).
thf(25334,plain,
( ( b @ i @ ( a @ rd ) )
!= ( unit @ i @ i ) ),
inference(rewrite,[status(thm)],[25173,802]) ).
thf(25345,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
!= ( b @ i @ ( a @ rd ) ) )
| ( A
!= ( unit @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1825,25334]) ).
thf(25364,plain,
! [A: $i] :
( ( ( unit @ i @ i @ ( A @ i @ mult ) @ i )
!= ( b @ i ) )
| ( A != a ) ),
inference(simp,[status(thm)],[25345]) ).
thf(25398,plain,
( ( unit @ i @ i @ ( a @ i @ mult ) @ i )
!= ( b @ i ) ),
inference(simp,[status(thm)],[25364]) ).
thf(26126,plain,
( ( unit @ ( a @ i @ mult ) @ i )
!= ( b @ i ) ),
inference(rewrite,[status(thm)],[25398,20045]) ).
thf(26169,plain,
( ( ( unit @ i )
!= ( a @ i ) )
| ( ( unit @ ( unit @ mult ) @ i )
!= ( b @ i ) ) ),
inference(paramod_ordered,[status(thm)],[43,26126]) ).
thf(26210,plain,
( ( unit != a )
| ( ( unit @ ( unit @ mult ) @ i )
!= ( b @ i ) ) ),
inference(simp,[status(thm)],[26169]) ).
thf(6053,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
!= ( C @ ( unit @ rd ) ) )
| ( A
= ( C @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1825,802]) ).
thf(6054,plain,
! [A: $i] :
( ( A @ ( unit @ i @ mult ) @ i @ i )
= A ),
inference(pattern_uni,[status(thm)],[6053:[bind(A,$thf( F )),bind(B,$thf( unit )),bind(C,$thf( F @ ( unit @ i @ mult ) @ i ))]]) ).
thf(6150,plain,
! [A: $i] :
( ( A @ ( unit @ i @ mult ) @ i @ i )
= A ),
inference(simp,[status(thm)],[6054]) ).
thf(6930,plain,
! [A: $i] :
( ( A @ ( unit @ i @ mult ) )
= A ),
inference(rewrite,[status(thm)],[6150,571]) ).
thf(6954,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( unit @ i @ mult ) )
!= ( B @ ( C @ mult ) @ i @ ( B @ mult ) ) )
| ( A
= ( C @ i ) ) ),
inference(paramod_ordered,[status(thm)],[6930,29]) ).
thf(6955,plain,
! [A: $i] :
( ( unit @ i @ ( A @ mult ) @ i )
= ( A @ i ) ),
inference(pattern_uni,[status(thm)],[6954:[bind(A,$thf( unit @ i @ ( F @ mult ) @ i )),bind(B,$thf( unit @ i )),bind(C,$thf( F ))]]) ).
thf(7313,plain,
! [A: $i] :
( ( unit @ i @ ( A @ mult ) @ i )
= ( A @ i ) ),
inference(simp,[status(thm)],[6955]) ).
thf(7904,plain,
! [A: $i] :
( ( unit @ ( A @ mult ) @ i )
= ( A @ i ) ),
inference(rewrite,[status(thm)],[7313,43]) ).
thf(46983,plain,
( ( unit != a )
| ( ( unit @ i )
!= ( b @ i ) ) ),
inference(rewrite,[status(thm)],[26210,7904]) ).
thf(11731,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ i ) )
| ( ( a @ ( A @ rd ) @ ( B @ mult ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[571,11030]) ).
thf(11732,plain,
! [A: $i] :
( ( a @ ( A @ rd ) @ ( A @ i @ mult ) )
!= b ),
inference(pattern_uni,[status(thm)],[11731:[bind(A,$thf( C )),bind(B,$thf( C @ i ))]]) ).
thf(11766,plain,
! [A: $i] :
( ( a @ ( A @ rd ) @ ( A @ i @ mult ) )
!= b ),
inference(simp,[status(thm)],[11732]) ).
thf(26522,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( a @ ( A @ rd ) @ ( unit @ mult ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[22320,11766]) ).
thf(26523,plain,
( ( a @ ( unit @ i @ i @ i @ i @ rd ) @ ( unit @ mult ) )
!= b ),
inference(pattern_uni,[status(thm)],[26522:[bind(A,$thf( unit @ i @ i @ i @ i ))]]) ).
thf(29914,plain,
( ( a @ ( unit @ i @ i @ i @ i @ rd ) )
!= b ),
inference(rewrite,[status(thm)],[26523,27]) ).
thf(11888,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[1829,11780]) ).
thf(11890,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[11888]) ).
thf(15293,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i @ i ) ),
inference(rewrite,[status(thm)],[11890,802]) ).
thf(15309,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A
!= ( unit @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1829,15293]) ).
thf(15332,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i @ i @ i @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[15309]) ).
thf(17446,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i @ i @ i @ i ) ),
inference(rewrite,[status(thm)],[15332,802]) ).
thf(17453,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A
!= ( unit @ i @ i @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1825,17446]) ).
thf(17469,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ ( A @ i @ mult ) @ i )
!= a )
| ( A
!= ( b @ i ) ) ),
inference(simp,[status(thm)],[17453]) ).
thf(17496,plain,
( ( unit @ i @ i @ i @ i @ ( b @ i @ i @ mult ) @ i )
!= a ),
inference(simp,[status(thm)],[17469]) ).
thf(19033,plain,
( ( unit @ i @ i @ ( b @ mult ) @ i )
!= a ),
inference(rewrite,[status(thm)],[17496,571]) ).
thf(19054,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ ( B @ mult ) )
!= ( unit @ i @ i @ ( b @ mult ) ) )
| ( ( B @ ( A @ rd ) @ i @ i )
!= a ) ),
inference(paramod_ordered,[status(thm)],[975,19033]) ).
thf(19055,plain,
( ( b @ ( unit @ i @ rd ) @ i @ i )
!= a ),
inference(pattern_uni,[status(thm)],[19054:[bind(A,$thf( unit @ i )),bind(B,$thf( b ))]]) ).
thf(19126,plain,
( ( b @ ( unit @ i @ rd ) )
!= a ),
inference(rewrite,[status(thm)],[19055,571]) ).
thf(19144,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( b @ ( unit @ i @ rd ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[1829,19126]) ).
thf(19145,plain,
( ( b @ ( unit @ i @ rd ) )
!= ( a @ i @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[19144]) ).
thf(19318,plain,
( ( b @ ( unit @ rd ) )
!= ( a @ i @ i ) ),
inference(rewrite,[status(thm)],[19145,802,43]) ).
thf(76479,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ ( b @ rd ) @ ( a @ mult ) @ i ) )
| ( A != B ) ),
inference(paramod_ordered,[status(thm)],[571,74356]) ).
thf(76539,plain,
! [A: $i] :
( ( A @ ( b @ rd ) @ ( a @ mult ) )
!= ( A @ i ) ),
inference(simp,[status(thm)],[76479]) ).
thf(76600,plain,
! [A: $i] :
( ( A @ ( b @ rd ) @ ( a @ mult ) )
!= ( A @ i ) ),
inference(simp,[status(thm)],[76539]) ).
thf(40350,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( b @ ( C @ rd ) @ ( C @ i @ mult ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[21,24962]) ).
thf(40415,plain,
! [B: $i,A: $i] :
( ( A
!= ( b @ ( B @ rd ) ) )
| ( ( A @ ( a @ rd ) )
!= ( B @ i ) ) ),
inference(simp,[status(thm)],[40350]) ).
thf(40440,plain,
! [A: $i] :
( ( b @ ( A @ rd ) @ ( a @ rd ) )
!= ( A @ i ) ),
inference(simp,[status(thm)],[40415]) ).
thf(41845,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ i @ ( A @ rd ) )
!= ( b @ ( B @ ( a @ rd ) @ i @ rd ) ) )
| ( unit != B ) ),
inference(paramod_ordered,[status(thm)],[19879,24968]) ).
thf(41922,plain,
! [A: $i] :
( ( ( A @ i @ i )
!= b )
| ( A
!= ( unit @ ( a @ rd ) @ i ) ) ),
inference(simp,[status(thm)],[41845]) ).
thf(41962,plain,
( ( unit @ ( a @ rd ) @ i @ i @ i )
!= b ),
inference(simp,[status(thm)],[41922]) ).
thf(43413,plain,
( ( unit @ ( a @ rd ) @ i )
!= b ),
inference(rewrite,[status(thm)],[41962,571]) ).
thf(579,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ mult ) @ ( A @ ld ) )
!= ( unit @ ( C @ ld ) ) )
| ( B
= ( C @ i ) ) ),
inference(paramod_ordered,[status(thm)],[19,532]) ).
thf(585,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ mult ) )
!= unit )
| ( A != C )
| ( B
= ( C @ i ) ) ),
inference(simp,[status(thm)],[579]) ).
thf(587,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) )
!= unit )
| ( A
= ( B @ i ) ) ),
inference(simp,[status(thm)],[585]) ).
thf(48411,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( B @ i ) )
| ( ( unit @ ( B @ ( A @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[11079,48409]) ).
thf(48412,plain,
! [A: $i] :
( ( unit @ ( A @ ( unit @ rd ) @ ( A @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48411:[bind(A,$thf( D )),bind(B,$thf( D @ ( unit @ rd ) ))]]) ).
thf(48691,plain,
! [A: $i] :
( ( unit @ ( A @ ( unit @ rd ) @ ( A @ mult ) @ rd ) )
= unit ),
inference(simp,[status(thm)],[48412]) ).
thf(86370,plain,
! [A: $i] :
( ( A @ ( unit @ rd ) @ ( A @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48691,713]) ).
thf(46880,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ rd ) @ i )
!= ( C @ ( b @ rd ) @ i ) )
| ( ( A @ i @ ( B @ mult ) )
!= ( a @ ( C @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[975,32795]) ).
thf(46881,plain,
! [A: $i] :
( ( b @ i @ ( A @ mult ) )
!= ( a @ ( A @ mult ) ) ),
inference(pattern_uni,[status(thm)],[46880:[bind(A,$thf( b )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(46950,plain,
! [A: $i] :
( ( b @ i @ ( A @ mult ) )
!= ( a @ ( A @ mult ) ) ),
inference(simp,[status(thm)],[46881]) ).
thf(68147,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( b @ i @ ( C @ mult ) ) )
| ( A
!= ( a @ ( C @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,46950]) ).
thf(68148,plain,
! [A: $i] :
( ( a @ ( b @ i @ ( A @ rd ) @ mult ) )
!= A ),
inference(pattern_uni,[status(thm)],[68147:[bind(A,$thf( D )),bind(B,$thf( b @ i )),bind(C,$thf( b @ i @ ( D @ rd ) ))]]) ).
thf(68290,plain,
! [A: $i] :
( ( a @ ( b @ i @ ( A @ rd ) @ mult ) )
!= A ),
inference(simp,[status(thm)],[68148]) ).
thf(86928,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ rd ) @ ( A @ mult ) )
!= ( a @ ( b @ i @ ( B @ rd ) @ mult ) ) )
| ( unit != B ) ),
inference(paramod_ordered,[status(thm)],[86370,68290]) ).
thf(87748,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) )
!= a )
| ( A
!= ( b @ i @ ( unit @ rd ) ) ) ),
inference(simp,[status(thm)],[86928]) ).
thf(88637,plain,
( ( b @ i @ ( unit @ rd ) @ ( unit @ rd ) )
!= a ),
inference(simp,[status(thm)],[87748]) ).
thf(94269,plain,
( ( b @ i @ ( unit @ rd ) @ i )
!= a ),
inference(rewrite,[status(thm)],[88637,802]) ).
thf(20936,plain,
! [B: $i,A: $i] :
( ( ( unit @ i @ i @ i )
!= ( B @ i ) )
| ( ( A @ ( unit @ rd ) @ ( B @ mult ) @ i )
= A ) ),
inference(paramod_ordered,[status(thm)],[20919,2316]) ).
thf(20937,plain,
! [A: $i] :
( ( A @ ( unit @ rd ) @ ( unit @ i @ i @ mult ) @ i )
= A ),
inference(pattern_uni,[status(thm)],[20936:[bind(A,$thf( A )),bind(B,$thf( unit @ i @ i ))]]) ).
thf(98555,plain,
! [A: $i] :
( ( A @ i @ ( unit @ mult ) @ i )
= A ),
inference(rewrite,[status(thm)],[20937,802,20045]) ).
thf(99036,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ rd ) @ i )
!= ( B @ i ) )
| ( ( unit @ ( unit @ mult ) @ i )
= B ) ),
inference(paramod_ordered,[status(thm)],[3288,98555]) ).
thf(99037,plain,
! [A: $i] :
( ( A @ ( A @ rd ) )
= ( unit @ ( unit @ mult ) @ i ) ),
inference(pattern_uni,[status(thm)],[99036:[bind(A,$thf( D )),bind(B,$thf( D @ ( D @ rd ) ))]]) ).
thf(99914,plain,
! [A: $i] :
( ( A @ ( A @ rd ) )
= ( unit @ ( unit @ mult ) @ i ) ),
inference(simp,[status(thm)],[99037]) ).
thf(105947,plain,
! [A: $i] :
( ( A @ ( A @ rd ) )
= ( unit @ i ) ),
inference(rewrite,[status(thm)],[99914,7904]) ).
thf(860,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ rd ) @ ld ) )
!= ( C @ ( C @ ld ) ) )
| ( B = unit ) ),
inference(paramod_ordered,[status(thm)],[712,525]) ).
thf(866,plain,
! [C: $i,B: $i,A: $i] :
( ( A != C )
| ( ( B @ ( A @ rd ) )
!= C )
| ( B = unit ) ),
inference(simp,[status(thm)],[860]) ).
thf(870,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ rd ) )
!= A )
| ( B = unit ) ),
inference(simp,[status(thm)],[866]) ).
thf(86386,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ rd ) @ ( A @ mult ) )
!= ( b @ i @ ( B @ mult ) ) )
| ( ( a @ ( unit @ rd ) )
!= B ) ),
inference(paramod_ordered,[status(thm)],[86370,32800]) ).
thf(87400,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) )
!= ( b @ i ) )
| ( A
!= ( a @ ( unit @ rd ) ) ) ),
inference(simp,[status(thm)],[86386]) ).
thf(88334,plain,
( ( a @ ( unit @ rd ) @ ( unit @ rd ) )
!= ( b @ i ) ),
inference(simp,[status(thm)],[87400]) ).
thf(94068,plain,
( ( a @ ( unit @ rd ) @ i )
!= ( b @ i ) ),
inference(rewrite,[status(thm)],[88334,802]) ).
thf(641,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( b != a )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[21,287]) ).
thf(682,plain,
! [A: $i] :
( ( ( A @ ( A @ ( unit @ rd ) @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( b != a ) ),
inference(simp,[status(thm)],[641]) ).
thf(733,plain,
! [A: $i] :
( ( ( A @ ( A @ ( unit @ rd ) @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( b != a ) ),
inference(simp,[status(thm)],[682]) ).
thf(81335,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( b != a ) ),
inference(rewrite,[status(thm)],[733,802]) ).
thf(62,plain,
! [A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( ( A @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,15]) ).
thf(141,plain,
! [A: $i] :
( ( unit != c )
| ( A
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( A @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[62]) ).
thf(152,plain,
( ( unit != c )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( a @ ( a @ ( b @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[141]) ).
thf(901,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( B @ i @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,15]) ).
thf(932,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( B @ i )
!= a ) ),
inference(simp,[status(thm)],[901]) ).
thf(100683,plain,
! [A: $i] :
( ( ( A @ i )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( A @ i )
!= a ) ),
inference(rewrite,[status(thm)],[932,29]) ).
thf(318,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( B != unit )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,174]) ).
thf(357,plain,
! [A: $i] :
( ( ( unit @ ( A @ ld ) )
!= b )
| ( A != a )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[318]) ).
thf(393,plain,
( ( ( unit @ ( a @ ld ) )
!= b )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[357]) ).
thf(44881,plain,
( ( ( a @ ( unit @ i @ mult ) @ i )
!= b )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[393,2318]) ).
thf(74,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( unit @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,15]) ).
thf(127,plain,
! [A: $i] :
( ( A != c )
| ( ( A @ i )
!= a )
| ( ( unit @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[74]) ).
thf(186,plain,
( ( ( c @ i )
!= a )
| ( ( unit @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[127]) ).
thf(21820,plain,
( ( ( c @ i )
!= a )
| ( ( a @ ( b @ ( a @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[186,25]) ).
thf(48550,plain,
! [A: $i] :
( ( ( unit @ i )
!= ( A @ i ) )
| ( ( unit @ ( A @ ( unit @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[43,48409]) ).
thf(48551,plain,
( ( unit @ ( unit @ ( unit @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48550:[bind(A,$thf( unit ))]]) ).
thf(48733,plain,
( ( unit @ ( unit @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48551,713]) ).
thf(84947,plain,
! [A: $i] :
( ( ( unit @ ( unit @ mult ) )
!= ( A @ ( a @ rd ) @ ( b @ mult ) ) )
| ( ( unit @ i )
!= A ) ),
inference(paramod_ordered,[status(thm)],[48733,76114]) ).
thf(84973,plain,
( ( ( unit @ i @ ( a @ rd ) )
!= unit )
| ( unit != b ) ),
inference(simp,[status(thm)],[84947]) ).
thf(85090,plain,
( ( ( unit @ ( a @ rd ) )
!= unit )
| ( unit != b ) ),
inference(rewrite,[status(thm)],[84973,43]) ).
thf(13042,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A
!= ( unit @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1829,13024]) ).
thf(13067,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i @ i @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[13042]) ).
thf(16335,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i @ i @ i ) ),
inference(rewrite,[status(thm)],[13067,802]) ).
thf(16350,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A
!= ( unit @ i @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[23,16335]) ).
thf(16371,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ ( unit @ i @ i @ i @ mult ) )
!= ( b @ i ) ) ),
inference(simp,[status(thm)],[16350]) ).
thf(16383,plain,
( ( a @ ( unit @ i @ i @ i @ mult ) )
!= ( b @ i ) ),
inference(simp,[status(thm)],[16371]) ).
thf(16386,plain,
( ( a @ ( unit @ i @ mult ) )
!= ( b @ i ) ),
inference(rewrite,[status(thm)],[16383,571]) ).
thf(86465,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ ( A @ mult ) )
!= ( a @ ( unit @ i @ mult ) ) )
| ( ( b @ i )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[86370,16386]) ).
thf(87889,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) )
!= a )
| ( A
!= ( unit @ i ) )
| ( ( b @ i )
!= unit ) ),
inference(simp,[status(thm)],[86465]) ).
thf(88765,plain,
( ( ( unit @ i @ ( unit @ rd ) )
!= a )
| ( ( b @ i )
!= unit ) ),
inference(simp,[status(thm)],[87889]) ).
thf(118341,plain,
( ( ( unit @ i @ i )
!= a )
| ( ( b @ i )
!= unit ) ),
inference(rewrite,[status(thm)],[88765,802]) ).
thf(26563,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( a @ ( C @ rd ) ) )
| ( ( A @ ( C @ i @ mult ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[23,11766]) ).
thf(26564,plain,
! [A: $i] :
( ( A @ ( a @ ( A @ mult ) @ i @ mult ) )
!= b ),
inference(pattern_uni,[status(thm)],[26563:[bind(A,$thf( D )),bind(B,$thf( a )),bind(C,$thf( a @ ( D @ mult ) ))]]) ).
thf(26591,plain,
! [A: $i] :
( ( A @ ( a @ ( A @ mult ) @ i @ mult ) )
!= b ),
inference(simp,[status(thm)],[26564]) ).
thf(45857,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( B @ ( a @ ( B @ mult ) @ i @ mult ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[27,26591]) ).
thf(45885,plain,
! [A: $i] :
( ( A != b )
| ( ( a @ ( A @ mult ) @ i )
!= unit ) ),
inference(simp,[status(thm)],[45857]) ).
thf(45928,plain,
( ( a @ ( b @ mult ) @ i )
!= unit ),
inference(simp,[status(thm)],[45885]) ).
thf(45973,plain,
! [A: $i] :
( ( ( A @ ( A @ rd ) @ i )
!= ( a @ ( b @ mult ) @ i ) )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[3288,45928]) ).
thf(45974,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ i )
!= ( a @ ( b @ mult ) @ i ) ),
inference(simp,[status(thm)],[45973]) ).
thf(46010,plain,
! [A: $i] :
( ( A @ ( A @ rd ) )
!= ( a @ ( b @ mult ) ) ),
inference(simp,[status(thm)],[45974]) ).
thf(32861,plain,
! [A: $i] :
( ( ( A @ ( A @ rd ) @ i )
!= ( a @ i @ ( b @ rd ) @ i ) )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[3288,32802]) ).
thf(32862,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ i )
!= ( a @ i @ ( b @ rd ) @ i ) ),
inference(simp,[status(thm)],[32861]) ).
thf(32892,plain,
! [A: $i] :
( ( A @ ( A @ rd ) )
!= ( a @ i @ ( b @ rd ) ) ),
inference(simp,[status(thm)],[32862]) ).
thf(47195,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( a @ i @ ( b @ rd ) ) )
| ( A
!= ( C @ ( C @ rd ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,32892]) ).
thf(47206,plain,
! [B: $i,A: $i] :
( ( A
!= ( a @ i ) )
| ( ( A @ ( B @ ( B @ rd ) @ mult ) )
!= b ) ),
inference(simp,[status(thm)],[47195]) ).
thf(47337,plain,
! [A: $i] :
( ( a @ i @ ( A @ ( A @ rd ) @ mult ) )
!= b ),
inference(simp,[status(thm)],[47206]) ).
thf(68804,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ ( B @ mult ) )
!= ( a @ i @ ( C @ ( C @ rd ) @ mult ) ) )
| ( ( B @ ( A @ rd ) @ i )
!= b ) ),
inference(paramod_ordered,[status(thm)],[975,47337]) ).
thf(68805,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ ( a @ rd ) @ i )
!= b ),
inference(pattern_uni,[status(thm)],[68804:[bind(A,$thf( a )),bind(B,$thf( E @ ( E @ rd ) )),bind(C,$thf( E ))]]) ).
thf(68892,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ ( a @ rd ) @ i )
!= b ),
inference(simp,[status(thm)],[68805]) ).
thf(75120,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ ( B @ rd ) @ ( a @ rd ) @ i ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[571,68892]) ).
thf(75137,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ ( a @ rd ) )
!= ( b @ i ) ),
inference(simp,[status(thm)],[75120]) ).
thf(75176,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ ( a @ rd ) )
!= ( b @ i ) ),
inference(simp,[status(thm)],[75137]) ).
thf(64,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( A @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,15]) ).
thf(97,plain,
! [A: $i] :
( ( A != b )
| ( unit != a )
| ( ( c @ ( a @ mult ) @ ( a @ ( A @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[64]) ).
thf(164,plain,
( ( unit != a )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(15308,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A
!= ( unit @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[23,15293]) ).
thf(15325,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ ( unit @ i @ i @ mult ) )
!= ( b @ i ) ) ),
inference(simp,[status(thm)],[15308]) ).
thf(15340,plain,
( ( a @ ( unit @ i @ i @ mult ) )
!= ( b @ i ) ),
inference(simp,[status(thm)],[15325]) ).
thf(15398,plain,
( ( a @ ( unit @ mult ) )
!= ( b @ i ) ),
inference(rewrite,[status(thm)],[15340,571]) ).
thf(41999,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ rd ) @ i )
!= ( b @ i @ ( a @ rd ) @ i ) )
| ( ( A @ i @ ( B @ mult ) )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[975,41963]) ).
thf(42000,plain,
( ( a @ i @ ( b @ i @ mult ) )
!= unit ),
inference(pattern_uni,[status(thm)],[41999:[bind(A,$thf( a )),bind(B,$thf( b @ i ))]]) ).
thf(76468,plain,
! [A: $i] :
( ( ( unit @ ( unit @ mult ) )
!= ( A @ ( b @ rd ) @ ( a @ mult ) ) )
| ( ( unit @ i )
!= A ) ),
inference(paramod_ordered,[status(thm)],[48733,74356]) ).
thf(76491,plain,
( ( ( unit @ i @ ( b @ rd ) )
!= unit )
| ( unit != a ) ),
inference(simp,[status(thm)],[76468]) ).
thf(77440,plain,
( ( ( unit @ ( b @ rd ) )
!= unit )
| ( unit != a ) ),
inference(rewrite,[status(thm)],[76491,43]) ).
thf(11718,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( a @ ( C @ i @ rd ) @ ( C @ mult ) ) )
| ( B != b ) ),
inference(paramod_ordered,[status(thm)],[17,11030]) ).
thf(11744,plain,
! [B: $i,A: $i] :
( ( ( b @ ( A @ ld ) )
!= ( a @ ( B @ i @ rd ) ) )
| ( A != B ) ),
inference(simp,[status(thm)],[11718]) ).
thf(11771,plain,
! [A: $i] :
( ( a @ ( A @ i @ rd ) )
!= ( b @ ( A @ ld ) ) ),
inference(simp,[status(thm)],[11744]) ).
thf(32256,plain,
! [A: $i] :
( ( a @ ( A @ i @ rd ) )
!= ( A @ ( b @ i @ mult ) @ i ) ),
inference(rewrite,[status(thm)],[11771,2318]) ).
thf(814,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( C @ ( C @ rd ) ) )
| ( A = unit ) ),
inference(paramod_ordered,[status(thm)],[23,782]) ).
thf(818,plain,
! [C: $i,B: $i,A: $i] :
( ( B != C )
| ( ( B @ ( A @ mult ) )
!= C )
| ( A = unit ) ),
inference(simp,[status(thm)],[814]) ).
thf(821,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ mult ) )
!= B )
| ( A = unit ) ),
inference(simp,[status(thm)],[818]) ).
thf(76439,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( B @ ( b @ rd ) @ ( a @ mult ) ) )
| ( ( unit @ i )
!= B ) ),
inference(paramod_ordered,[status(thm)],[37,74356]) ).
thf(76509,plain,
! [A: $i] :
( ( ( A @ i )
!= ( unit @ i @ ( b @ rd ) ) )
| ( A != a ) ),
inference(simp,[status(thm)],[76439]) ).
thf(76595,plain,
( ( unit @ i @ ( b @ rd ) )
!= ( a @ i ) ),
inference(simp,[status(thm)],[76509]) ).
thf(76604,plain,
( ( unit @ ( b @ rd ) )
!= ( a @ i ) ),
inference(rewrite,[status(thm)],[76595,43]) ).
thf(14136,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( B @ i ) )
| ( ( B @ ( A @ mult ) @ i )
= unit ) ),
inference(paramod_ordered,[status(thm)],[11079,13737]) ).
thf(14137,plain,
! [A: $i] :
( ( A @ ( unit @ rd ) @ ( A @ mult ) @ i )
= unit ),
inference(pattern_uni,[status(thm)],[14136:[bind(A,$thf( D )),bind(B,$thf( D @ ( unit @ rd ) ))]]) ).
thf(14280,plain,
! [A: $i] :
( ( A @ ( unit @ rd ) @ ( A @ mult ) @ i )
= unit ),
inference(simp,[status(thm)],[14137]) ).
thf(16448,plain,
! [A: $i] :
( ( A @ i @ ( A @ mult ) @ i )
= unit ),
inference(rewrite,[status(thm)],[14280,802]) ).
thf(47052,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( b @ i @ ( C @ mult ) ) )
| ( ( a @ ( A @ rd ) )
!= C ) ),
inference(paramod_ordered,[status(thm)],[21,32800]) ).
thf(47053,plain,
! [A: $i] :
( ( b @ i @ ( A @ rd ) )
!= ( a @ ( A @ rd ) ) ),
inference(pattern_uni,[status(thm)],[47052:[bind(A,$thf( D )),bind(B,$thf( b @ i )),bind(C,$thf( b @ i @ ( D @ rd ) ))]]) ).
thf(47149,plain,
! [A: $i] :
( ( b @ i @ ( A @ rd ) )
!= ( a @ ( A @ rd ) ) ),
inference(simp,[status(thm)],[47053]) ).
thf(47946,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( b @ ( C @ mult ) ) )
| ( A
!= ( C @ ( a @ rd ) @ i ) ) ),
inference(paramod_ordered,[status(thm)],[21,41955]) ).
thf(47947,plain,
! [A: $i] :
( ( b @ ( A @ rd ) @ ( a @ rd ) @ i )
!= A ),
inference(pattern_uni,[status(thm)],[47946:[bind(A,$thf( D )),bind(B,$thf( b )),bind(C,$thf( b @ ( D @ rd ) ))]]) ).
thf(48049,plain,
! [A: $i] :
( ( b @ ( A @ rd ) @ ( a @ rd ) @ i )
!= A ),
inference(simp,[status(thm)],[47947]) ).
thf(71661,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ rd ) @ i )
!= ( b @ ( C @ rd ) @ ( a @ rd ) @ i ) )
| ( ( A @ i @ ( B @ mult ) )
!= C ) ),
inference(paramod_ordered,[status(thm)],[975,48049]) ).
thf(71662,plain,
! [A: $i] :
( ( a @ i @ ( b @ ( A @ rd ) @ mult ) )
!= A ),
inference(pattern_uni,[status(thm)],[71661:[bind(A,$thf( a )),bind(B,$thf( b @ ( D @ rd ) )),bind(C,$thf( D ))]]) ).
thf(71781,plain,
! [A: $i] :
( ( a @ i @ ( b @ ( A @ rd ) @ mult ) )
!= A ),
inference(simp,[status(thm)],[71662]) ).
thf(298,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( C @ ( unit @ mult ) ) )
| ( B = C ) ),
inference(paramod_ordered,[status(thm)],[17,27]) ).
thf(299,plain,
! [A: $i] :
( ( A @ ( unit @ ld ) )
= A ),
inference(pattern_uni,[status(thm)],[298:[bind(A,$thf( unit )),bind(B,$thf( E )),bind(C,$thf( E @ ( unit @ ld ) ))]]) ).
thf(397,plain,
! [A: $i] :
( ( A @ ( unit @ ld ) )
= A ),
inference(simp,[status(thm)],[299]) ).
thf(858,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ rd ) @ ld ) )
!= ( C @ ( unit @ ld ) ) )
| ( B = C ) ),
inference(paramod_ordered,[status(thm)],[712,397]) ).
thf(863,plain,
! [C: $i,B: $i,A: $i] :
( ( A != C )
| ( ( B @ ( A @ rd ) )
!= unit )
| ( B = C ) ),
inference(simp,[status(thm)],[858]) ).
thf(877,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ rd ) )
!= unit )
| ( A = B ) ),
inference(simp,[status(thm)],[863]) ).
thf(304,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( C @ ( C @ i @ mult ) ) )
| ( B = unit ) ),
inference(paramod_ordered,[status(thm)],[17,35]) ).
thf(364,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= C )
| ( A
!= ( C @ i ) )
| ( B = unit ) ),
inference(simp,[status(thm)],[304]) ).
thf(399,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ ld ) )
!= B )
| ( A = unit ) ),
inference(simp,[status(thm)],[364]) ).
thf(46098,plain,
! [B: $i,A: $i] :
( ( ( B @ i @ ( A @ i @ mult ) @ i )
!= B )
| ( A = unit ) ),
inference(rewrite,[status(thm)],[399,2318]) ).
thf(902,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( B @ i @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,15]) ).
thf(954,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= b )
| ( A != a )
| ( ( c @ ( a @ mult ) @ ( a @ ( B @ i @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[902]) ).
thf(998,plain,
! [A: $i] :
( ( ( a @ ( A @ mult ) @ i )
!= b )
| ( ( c @ ( a @ mult ) @ ( a @ ( A @ i @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[954]) ).
thf(45958,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) @ i )
!= ( a @ ( b @ mult ) @ i ) )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[13737,45928]) ).
thf(45959,plain,
! [A: $i] :
( ( A @ ( A @ i @ mult ) @ i )
!= ( a @ ( b @ mult ) @ i ) ),
inference(simp,[status(thm)],[45958]) ).
thf(45987,plain,
! [A: $i] :
( ( A @ ( A @ i @ mult ) )
!= ( a @ ( b @ mult ) ) ),
inference(simp,[status(thm)],[45959]) ).
thf(48332,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( C @ ( C @ i @ mult ) ) )
| ( A
!= ( a @ ( b @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,45987]) ).
thf(48383,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ ( a @ ( b @ mult ) @ rd ) )
!= ( B @ i ) ) ),
inference(simp,[status(thm)],[48332]) ).
thf(48403,plain,
! [A: $i] :
( ( A @ ( a @ ( b @ mult ) @ rd ) )
!= ( A @ i ) ),
inference(simp,[status(thm)],[48383]) ).
thf(11723,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( a @ ( B @ i @ rd ) @ ( B @ mult ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[27,11030]) ).
thf(11724,plain,
( ( a @ ( unit @ i @ rd ) )
!= b ),
inference(pattern_uni,[status(thm)],[11723:[bind(A,$thf( a @ ( unit @ i @ rd ) )),bind(B,$thf( unit ))]]) ).
thf(11792,plain,
( ( a @ ( unit @ rd ) )
!= b ),
inference(rewrite,[status(thm)],[11724,43]) ).
thf(11802,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( a @ ( unit @ rd ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[1829,11792]) ).
thf(11805,plain,
( ( b @ i @ ( unit @ rd ) )
!= ( a @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[11802]) ).
thf(12744,plain,
( ( b @ i @ i )
!= ( a @ i ) ),
inference(rewrite,[status(thm)],[11805,802]) ).
thf(12750,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( b @ i @ i ) )
| ( A
!= ( a @ i ) ) ),
inference(paramod_ordered,[status(thm)],[11079,12744]) ).
thf(12769,plain,
( ( a @ i @ ( unit @ rd ) )
!= ( b @ i ) ),
inference(simp,[status(thm)],[12750]) ).
thf(12907,plain,
( ( a @ i @ i )
!= ( b @ i ) ),
inference(rewrite,[status(thm)],[12769,802]) ).
thf(26537,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( a @ ( A @ rd ) @ ( unit @ mult ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[22781,11766]) ).
thf(26538,plain,
( ( a @ ( unit @ i @ i @ i @ i @ i @ rd ) @ ( unit @ mult ) )
!= b ),
inference(pattern_uni,[status(thm)],[26537:[bind(A,$thf( unit @ i @ i @ i @ i @ i ))]]) ).
thf(32023,plain,
( ( a @ ( unit @ i @ i @ i @ i @ i @ rd ) )
!= b ),
inference(rewrite,[status(thm)],[26538,27]) ).
thf(933,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= a )
| ( A
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( B @ i @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[901]) ).
thf(981,plain,
! [A: $i] :
( ( ( b @ ( a @ mult ) @ ( A @ mult ) @ i )
!= a )
| ( ( c @ ( a @ mult ) @ ( A @ i @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[933]) ).
thf(763,plain,
( ( ( unit @ i )
!= ( a @ i ) )
| ( unit != b ) ),
inference(paramod_ordered,[status(thm)],[43,630]) ).
thf(766,plain,
( ( unit != a )
| ( unit != b ) ),
inference(simp,[status(thm)],[763]) ).
thf(40391,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( b @ ( C @ rd ) ) )
| ( ( A @ ( C @ i @ mult ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[23,24962]) ).
thf(40392,plain,
! [A: $i] :
( ( A @ ( b @ ( A @ mult ) @ i @ mult ) )
!= a ),
inference(pattern_uni,[status(thm)],[40391:[bind(A,$thf( D )),bind(B,$thf( b )),bind(C,$thf( b @ ( D @ mult ) ))]]) ).
thf(40421,plain,
! [A: $i] :
( ( A @ ( b @ ( A @ mult ) @ i @ mult ) )
!= a ),
inference(simp,[status(thm)],[40392]) ).
thf(47571,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ i @ mult ) )
!= ( b @ ( B @ mult ) ) )
| ( ( B @ ( A @ i @ mult ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[6930,40421]) ).
thf(47572,plain,
( ( unit @ i @ ( b @ i @ mult ) )
!= a ),
inference(pattern_uni,[status(thm)],[47571:[bind(A,$thf( b )),bind(B,$thf( unit @ i ))]]) ).
thf(47644,plain,
( ( unit @ ( b @ i @ mult ) )
!= a ),
inference(rewrite,[status(thm)],[47572,43]) ).
thf(86298,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ i ) )
| ( ( A @ ( b @ rd ) @ ( B @ rd ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[571,76588]) ).
thf(86299,plain,
! [A: $i] :
( ( A @ ( b @ rd ) @ ( A @ i @ rd ) )
!= a ),
inference(pattern_uni,[status(thm)],[86298:[bind(A,$thf( C )),bind(B,$thf( C @ i ))]]) ).
thf(86342,plain,
! [A: $i] :
( ( A @ ( b @ rd ) @ ( A @ i @ rd ) )
!= a ),
inference(simp,[status(thm)],[86299]) ).
thf(95427,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ ( b @ rd ) @ ( unit @ rd ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[22781,86342]) ).
thf(95428,plain,
( ( unit @ i @ i @ i @ i @ i @ ( b @ rd ) @ ( unit @ rd ) )
!= a ),
inference(pattern_uni,[status(thm)],[95427:[bind(A,$thf( unit @ i @ i @ i @ i @ i ))]]) ).
thf(105032,plain,
( ( unit @ i @ i @ i @ i @ i @ ( b @ rd ) @ i )
!= a ),
inference(rewrite,[status(thm)],[95428,802]) ).
thf(48475,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( unit @ ( A @ ( unit @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[25423,48409]) ).
thf(48476,plain,
( ( unit @ ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ ( unit @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48475:[bind(A,$thf( unit @ i @ i @ i @ i @ i @ i @ i @ i ))]]) ).
thf(65334,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ ( unit @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48476,713]) ).
thf(32839,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ rd ) @ i )
!= ( a @ i @ ( b @ rd ) @ i ) )
| ( ( A @ i @ ( B @ mult ) )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[975,32802]) ).
thf(32840,plain,
( ( b @ i @ ( a @ i @ mult ) )
!= unit ),
inference(pattern_uni,[status(thm)],[32839:[bind(A,$thf( b )),bind(B,$thf( a @ i ))]]) ).
thf(45858,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ i @ mult ) )
!= ( a @ ( B @ mult ) ) )
| ( ( B @ ( A @ i @ mult ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[6930,26591]) ).
thf(45859,plain,
( ( unit @ i @ ( a @ i @ mult ) )
!= b ),
inference(pattern_uni,[status(thm)],[45858:[bind(A,$thf( a )),bind(B,$thf( unit @ i ))]]) ).
thf(46025,plain,
( ( unit @ ( a @ i @ mult ) )
!= b ),
inference(rewrite,[status(thm)],[45859,43]) ).
thf(647,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( A @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,15]) ).
thf(696,plain,
! [B: $i,A: $i] :
( ( B != c )
| ( ( B @ ( A @ rd ) )
!= a )
| ( ( A @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[647]) ).
thf(746,plain,
! [A: $i] :
( ( ( c @ ( A @ rd ) )
!= a )
| ( ( A @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[696]) ).
thf(881,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( C @ ( D @ mult ) @ i @ ( C @ mult ) ) )
| ( B
= ( D @ i ) ) ),
inference(paramod_ordered,[status(thm)],[17,29]) ).
thf(956,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= ( C @ ( D @ mult ) @ i ) )
| ( A != C )
| ( B
= ( D @ i ) ) ),
inference(simp,[status(thm)],[881]) ).
thf(1000,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ld ) )
!= ( B @ ( C @ mult ) @ i ) )
| ( A
= ( C @ i ) ) ),
inference(simp,[status(thm)],[956]) ).
thf(116864,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ i @ mult ) @ i )
!= ( B @ ( C @ mult ) @ i ) )
| ( A
= ( C @ i ) ) ),
inference(rewrite,[status(thm)],[1000,2318]) ).
thf(3615,plain,
! [A: $i] :
( ( ( A @ ( A @ rd ) @ i )
!= ( a @ i ) )
| ( unit != b ) ),
inference(paramod_ordered,[status(thm)],[3288,630]) ).
thf(3652,plain,
! [A: $i] :
( ( ( A @ ( A @ rd ) )
!= a )
| ( unit != b ) ),
inference(simp,[status(thm)],[3615]) ).
thf(3974,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( B @ ( B @ rd ) ) )
| ( A != a )
| ( unit != b ) ),
inference(paramod_ordered,[status(thm)],[1829,3652]) ).
thf(3983,plain,
! [A: $i] :
( ( ( a @ i )
!= A )
| ( unit != A )
| ( unit != b ) ),
inference(simp,[status(thm)],[3974]) ).
thf(3992,plain,
( ( ( a @ i )
!= unit )
| ( unit != b ) ),
inference(simp,[status(thm)],[3983]) ).
thf(11148,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( a @ i ) )
| ( A != unit )
| ( unit != b ) ),
inference(paramod_ordered,[status(thm)],[11079,3992]) ).
thf(11179,plain,
( ( ( unit @ ( unit @ rd ) )
!= a )
| ( unit != b ) ),
inference(simp,[status(thm)],[11148]) ).
thf(11217,plain,
( ( ( unit @ i )
!= a )
| ( unit != b ) ),
inference(rewrite,[status(thm)],[11179,802]) ).
thf(18078,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( C @ ( C @ rd ) ) )
| ( A
!= ( b @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,13811]) ).
thf(18084,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ ( b @ ( a @ mult ) @ mult ) )
!= B ) ),
inference(simp,[status(thm)],[18078]) ).
thf(18091,plain,
! [A: $i] :
( ( A @ ( b @ ( a @ mult ) @ mult ) )
!= A ),
inference(simp,[status(thm)],[18084]) ).
thf(48570,plain,
! [A: $i] :
( ( ( unit @ i @ i )
!= ( A @ i ) )
| ( ( unit @ ( A @ ( unit @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[20045,48409]) ).
thf(48571,plain,
( ( unit @ ( unit @ i @ ( unit @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48570:[bind(A,$thf( unit @ i ))]]) ).
thf(50298,plain,
( ( unit @ i @ ( unit @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48571,713]) ).
thf(76066,plain,
! [A: $i] :
( ( ( A @ ( A @ ( a @ rd ) @ mult ) )
!= ( unit @ i @ ( unit @ mult ) ) )
| ( ( b @ i )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[50298,71555]) ).
thf(76082,plain,
! [A: $i] :
( ( A
!= ( unit @ i ) )
| ( ( A @ ( a @ rd ) )
!= unit )
| ( ( b @ i )
!= unit ) ),
inference(simp,[status(thm)],[76066]) ).
thf(76127,plain,
( ( ( unit @ i @ ( a @ rd ) )
!= unit )
| ( ( b @ i )
!= unit ) ),
inference(simp,[status(thm)],[76082]) ).
thf(114252,plain,
( ( ( unit @ ( a @ rd ) )
!= unit )
| ( ( b @ i )
!= unit ) ),
inference(rewrite,[status(thm)],[76127,43]) ).
thf(650,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( c @ ( A @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,15]) ).
thf(678,plain,
! [B: $i,A: $i] :
( ( B != a )
| ( ( B @ ( A @ rd ) )
!= ( a @ ( b @ mult ) ) )
| ( ( c @ ( A @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[650]) ).
thf(729,plain,
! [A: $i] :
( ( ( a @ ( A @ rd ) )
!= ( a @ ( b @ mult ) ) )
| ( ( c @ ( A @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[678]) ).
thf(552,plain,
! [C: $i,B: $i,A: $i] :
( ( ( unit @ ( A @ i @ ld ) )
!= ( C @ ( B @ mult ) @ ( B @ ld ) ) )
| ( A = C ) ),
inference(paramod_ordered,[status(thm)],[531,19]) ).
thf(557,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ mult ) )
!= unit )
| ( ( A @ i )
!= B )
| ( A = C ) ),
inference(simp,[status(thm)],[552]) ).
thf(566,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ i @ mult ) )
!= unit )
| ( A = B ) ),
inference(simp,[status(thm)],[557]) ).
thf(953,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( B @ i @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[902]) ).
thf(101627,plain,
! [A: $i] :
( ( ( A @ i )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( A @ i @ mult ) )
!= a ) ),
inference(rewrite,[status(thm)],[953,29]) ).
thf(307,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( B @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,15]) ).
thf(331,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= a )
| ( A
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( B != a ) ),
inference(simp,[status(thm)],[307]) ).
thf(373,plain,
( ( ( a @ ( b @ ( a @ mult ) @ ld ) )
!= a )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[331]) ).
thf(37498,plain,
( ( ( b @ ( a @ mult ) @ ( a @ i @ mult ) @ i )
!= a )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[373,2318]) ).
thf(320,plain,
! [C: $i,B: $i,A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( C @ ( B @ ld ) @ ( B @ mult ) ) )
| ( A = C ) ),
inference(paramod_ordered,[status(thm)],[25,17]) ).
thf(354,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ld ) )
!= unit )
| ( A != B )
| ( A = C ) ),
inference(simp,[status(thm)],[320]) ).
thf(391,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= unit )
| ( A = B ) ),
inference(simp,[status(thm)],[354]) ).
thf(44103,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i )
!= unit )
| ( A = B ) ),
inference(rewrite,[status(thm)],[391,2318]) ).
thf(40343,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( b @ ( A @ rd ) @ ( unit @ mult ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[22320,24962]) ).
thf(40344,plain,
( ( b @ ( unit @ i @ i @ i @ i @ rd ) @ ( unit @ mult ) )
!= a ),
inference(pattern_uni,[status(thm)],[40343:[bind(A,$thf( unit @ i @ i @ i @ i ))]]) ).
thf(41384,plain,
( ( b @ ( unit @ i @ i @ i @ i @ rd ) )
!= a ),
inference(rewrite,[status(thm)],[40344,27]) ).
thf(26552,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i )
!= ( A @ i ) )
| ( ( a @ ( A @ rd ) @ ( unit @ mult ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[20919,11766]) ).
thf(26553,plain,
( ( a @ ( unit @ i @ i @ rd ) @ ( unit @ mult ) )
!= b ),
inference(pattern_uni,[status(thm)],[26552:[bind(A,$thf( unit @ i @ i ))]]) ).
thf(27754,plain,
( ( a @ ( unit @ i @ i @ rd ) )
!= b ),
inference(rewrite,[status(thm)],[26553,27]) ).
thf(21025,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i )
!= ( A @ i ) )
| ( ( a @ ( unit @ rd ) @ ( A @ mult ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[20919,11030]) ).
thf(21026,plain,
( ( a @ ( unit @ rd ) @ ( unit @ i @ i @ mult ) )
!= b ),
inference(pattern_uni,[status(thm)],[21025:[bind(A,$thf( unit @ i @ i ))]]) ).
thf(22183,plain,
( ( a @ i @ ( unit @ mult ) )
!= b ),
inference(rewrite,[status(thm)],[21026,802,20045]) ).
thf(22191,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( a @ i @ ( unit @ mult ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[21,22183]) ).
thf(22226,plain,
! [A: $i] :
( ( A
!= ( a @ i ) )
| ( ( A @ ( b @ rd ) )
!= unit ) ),
inference(simp,[status(thm)],[22191]) ).
thf(22235,plain,
( ( a @ i @ ( b @ rd ) )
!= unit ),
inference(simp,[status(thm)],[22226]) ).
thf(22263,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( a @ i @ ( b @ rd ) ) )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[1829,22235]) ).
thf(22291,plain,
( ( unit @ i @ ( unit @ rd ) )
!= ( a @ i @ ( b @ rd ) ) ),
inference(simp,[status(thm)],[22263]) ).
thf(22686,plain,
( ( a @ i @ ( b @ rd ) )
!= ( unit @ i @ i ) ),
inference(rewrite,[status(thm)],[22291,802]) ).
thf(22709,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( a @ i @ ( b @ rd ) ) )
| ( A
!= ( unit @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1829,22686]) ).
thf(22719,plain,
( ( unit @ i @ i @ i @ ( unit @ rd ) )
!= ( a @ i @ ( b @ rd ) ) ),
inference(simp,[status(thm)],[22709]) ).
thf(23604,plain,
( ( a @ i @ ( b @ rd ) )
!= ( unit @ i @ i @ i @ i ) ),
inference(rewrite,[status(thm)],[22719,802]) ).
thf(56,plain,
! [A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( A @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,15]) ).
thf(83,plain,
! [A: $i] :
( ( unit != b )
| ( A != a )
| ( ( c @ ( a @ mult ) @ ( a @ ( A @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[56]) ).
thf(156,plain,
( ( unit != b )
| ( ( c @ ( a @ mult ) @ ( a @ ( a @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[83]) ).
thf(26565,plain,
! [A: $i] :
( ( ( unit @ i @ i )
!= ( A @ i ) )
| ( ( a @ ( A @ rd ) @ ( unit @ mult ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[20045,11766]) ).
thf(26566,plain,
( ( a @ ( unit @ i @ rd ) @ ( unit @ mult ) )
!= b ),
inference(pattern_uni,[status(thm)],[26565:[bind(A,$thf( unit @ i ))]]) ).
thf(26620,plain,
( ( a @ ( unit @ i @ rd ) )
!= b ),
inference(rewrite,[status(thm)],[26566,27]) ).
thf(310,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( B @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,15]) ).
thf(343,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= c )
| ( A != a )
| ( ( B @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[310]) ).
thf(381,plain,
! [A: $i] :
( ( ( A @ ( a @ ld ) )
!= c )
| ( ( A @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[343]) ).
thf(39667,plain,
! [A: $i] :
( ( ( a @ ( A @ i @ mult ) @ i )
!= c )
| ( ( A @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[381,2318]) ).
thf(314,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( ( B @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,15]) ).
thf(346,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= c )
| ( A
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( B @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[314]) ).
thf(384,plain,
! [A: $i] :
( ( ( A @ ( a @ ( a @ ( b @ mult ) @ mult ) @ ld ) )
!= c )
| ( ( A @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[346]) ).
thf(40728,plain,
! [A: $i] :
( ( ( a @ ( a @ ( b @ mult ) @ mult ) @ ( A @ i @ mult ) @ i )
!= c )
| ( ( A @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(rewrite,[status(thm)],[384,2318]) ).
thf(914,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( B @ ( C @ mult ) @ i @ ( B @ mult ) ) )
| ( ( C @ i )
= unit ) ),
inference(paramod_ordered,[status(thm)],[37,29]) ).
thf(943,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i )
!= ( B @ ( C @ mult ) @ i ) )
| ( A != B )
| ( ( C @ i )
= unit ) ),
inference(simp,[status(thm)],[914]) ).
thf(989,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= ( A @ i ) )
| ( ( B @ i )
= unit ) ),
inference(simp,[status(thm)],[943]) ).
thf(644,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,15]) ).
thf(692,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( A != a ) ),
inference(simp,[status(thm)],[644]) ).
thf(742,plain,
! [A: $i] :
( ( ( A @ ( A @ ( a @ rd ) @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[692]) ).
thf(72817,plain,
! [A: $i] :
( ( ( a @ ( b @ i @ ( A @ rd ) @ mult ) )
!= ( unit @ ( unit @ mult ) ) )
| ( unit != A ) ),
inference(paramod_ordered,[status(thm)],[48733,68290]) ).
thf(72896,plain,
( ( a @ ( b @ i @ ( unit @ rd ) @ mult ) )
!= ( unit @ ( unit @ mult ) ) ),
inference(simp,[status(thm)],[72817]) ).
thf(74118,plain,
( ( a @ ( b @ i @ i @ mult ) )
!= unit ),
inference(rewrite,[status(thm)],[72896,802,48733]) ).
thf(26530,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( a @ ( A @ rd ) @ ( unit @ mult ) )
!= b ) ),
inference(paramod_ordered,[status(thm)],[21498,11766]) ).
thf(26531,plain,
( ( a @ ( unit @ i @ i @ i @ rd ) @ ( unit @ mult ) )
!= b ),
inference(pattern_uni,[status(thm)],[26530:[bind(A,$thf( unit @ i @ i @ i ))]]) ).
thf(28713,plain,
( ( a @ ( unit @ i @ i @ i @ rd ) )
!= b ),
inference(rewrite,[status(thm)],[26531,27]) ).
thf(425,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( unit @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,15]) ).
thf(467,plain,
! [A: $i] :
( ( ( A @ i )
!= a )
| ( A
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( unit @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[425]) ).
thf(493,plain,
( ( ( b @ ( a @ mult ) @ i )
!= a )
| ( ( c @ ( a @ mult ) @ ( unit @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[467]) ).
thf(57367,plain,
( ( ( b @ ( a @ mult ) @ i )
!= a )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[493,27]) ).
thf(634,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( D @ ( D @ ( C @ rd ) @ mult ) ) )
| ( B = C ) ),
inference(paramod_ordered,[status(thm)],[17,21]) ).
thf(676,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= D )
| ( A
!= ( D @ ( C @ rd ) ) )
| ( B = C ) ),
inference(simp,[status(thm)],[634]) ).
thf(728,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ rd ) @ ld ) )
!= C )
| ( A = B ) ),
inference(simp,[status(thm)],[676]) ).
thf(78606,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ rd ) @ ( A @ i @ mult ) @ i )
!= C )
| ( A = B ) ),
inference(rewrite,[status(thm)],[728,2318]) ).
thf(915,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( B @ ( C @ mult ) ) )
| ( ( unit @ i @ ( B @ mult ) )
= ( C @ i ) ) ),
inference(paramod_ordered,[status(thm)],[37,29]) ).
thf(916,plain,
! [A: $i] :
( ( unit @ i @ ( A @ i @ mult ) )
= ( A @ i ) ),
inference(pattern_uni,[status(thm)],[915:[bind(A,$thf( D )),bind(B,$thf( D @ i )),bind(C,$thf( D ))]]) ).
thf(974,plain,
! [A: $i] :
( ( unit @ i @ ( A @ i @ mult ) )
= ( A @ i ) ),
inference(simp,[status(thm)],[916]) ).
thf(1207,plain,
! [A: $i] :
( ( unit @ ( A @ i @ mult ) )
= ( A @ i ) ),
inference(rewrite,[status(thm)],[974,43]) ).
thf(94089,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ rd ) @ i )
!= ( a @ ( unit @ rd ) @ i ) )
| ( ( A @ i @ ( B @ mult ) )
!= ( b @ i ) ) ),
inference(paramod_ordered,[status(thm)],[975,94068]) ).
thf(94090,plain,
( ( unit @ i @ ( a @ mult ) )
!= ( b @ i ) ),
inference(pattern_uni,[status(thm)],[94089:[bind(A,$thf( unit )),bind(B,$thf( a ))]]) ).
thf(94190,plain,
( ( unit @ ( a @ mult ) )
!= ( b @ i ) ),
inference(rewrite,[status(thm)],[94090,43]) ).
thf(427,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[37,15]) ).
thf(460,plain,
! [A: $i] :
( ( ( A @ i )
!= ( c @ ( a @ mult ) ) )
| ( A
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[427]) ).
thf(488,plain,
( ( ( a @ ( b @ ( a @ mult ) @ mult ) @ i )
!= ( c @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[460]) ).
thf(20966,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i )
!= ( A @ i ) )
| ( ( unit @ i @ ( A @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[20919,19879]) ).
thf(20967,plain,
( ( unit @ i @ ( unit @ i @ i @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[20966:[bind(A,$thf( unit @ i @ i ))]]) ).
thf(21387,plain,
( ( unit @ ( unit @ rd ) )
= unit ),
inference(rewrite,[status(thm)],[20967,43,20045]) ).
thf(32723,plain,
! [A: $i] :
( ( ( unit @ ( unit @ rd ) )
!= ( A @ ( b @ rd ) ) )
| ( ( a @ ( unit @ i @ rd ) )
!= A ) ),
inference(paramod_ordered,[status(thm)],[21387,11786]) ).
thf(32729,plain,
( ( unit @ ( unit @ rd ) )
!= ( a @ ( unit @ i @ rd ) @ ( b @ rd ) ) ),
inference(simp,[status(thm)],[32723]) ).
thf(34189,plain,
( ( a @ ( unit @ rd ) @ ( b @ rd ) )
!= unit ),
inference(rewrite,[status(thm)],[32729,43,21387]) ).
thf(72,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( unit @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,15]) ).
thf(112,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( unit @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[72]) ).
thf(6303,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( a != a ) ),
inference(rewrite,[status(thm)],[112,27]) ).
thf(6304,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[6303]) ).
thf(313,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( c @ ( B @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,15]) ).
thf(340,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= a )
| ( A
!= ( a @ ( b @ mult ) ) )
| ( ( c @ ( B @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[313]) ).
thf(378,plain,
! [A: $i] :
( ( ( A @ ( a @ ( b @ mult ) @ ld ) )
!= a )
| ( ( c @ ( A @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[340]) ).
thf(39005,plain,
! [A: $i] :
( ( ( a @ ( b @ mult ) @ ( A @ i @ mult ) @ i )
!= a )
| ( ( c @ ( A @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(rewrite,[status(thm)],[378,2318]) ).
thf(898,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( b != a )
| ( ( B @ i )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[29,287]) ).
thf(952,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= b )
| ( A != a )
| ( b != a )
| ( ( B @ i )
!= unit ) ),
inference(simp,[status(thm)],[898]) ).
thf(997,plain,
! [A: $i] :
( ( ( a @ ( A @ mult ) @ i )
!= b )
| ( b != a )
| ( ( A @ i )
!= unit ) ),
inference(simp,[status(thm)],[952]) ).
thf(904,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( B @ i @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,15]) ).
thf(938,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= c )
| ( A != a )
| ( ( B @ i @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[904]) ).
thf(985,plain,
! [A: $i] :
( ( ( a @ ( A @ mult ) @ i )
!= c )
| ( ( A @ i @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[938]) ).
thf(19133,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
!= ( b @ ( unit @ i @ rd ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[1825,19126]) ).
thf(19155,plain,
! [A: $i] :
( ( ( a @ ( A @ i @ mult ) @ i )
!= b )
| ( A
!= ( unit @ i ) ) ),
inference(simp,[status(thm)],[19133]) ).
thf(19168,plain,
( ( a @ ( unit @ i @ i @ mult ) @ i )
!= b ),
inference(simp,[status(thm)],[19155]) ).
thf(19181,plain,
( ( a @ ( unit @ mult ) @ i )
!= b ),
inference(rewrite,[status(thm)],[19168,571]) ).
thf(46985,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( unit @ i ) )
| ( unit != a )
| ( A
!= ( b @ i ) ) ),
inference(paramod_ordered,[status(thm)],[11079,46983]) ).
thf(47021,plain,
( ( ( b @ i @ ( unit @ rd ) )
!= unit )
| ( unit != a ) ),
inference(simp,[status(thm)],[46985]) ).
thf(47432,plain,
( ( ( b @ i @ i )
!= unit )
| ( unit != a ) ),
inference(rewrite,[status(thm)],[47021,802]) ).
thf(906,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) )
| ( ( B @ i )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,15]) ).
thf(936,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( A != a )
| ( ( B @ i )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[906]) ).
thf(984,plain,
! [A: $i] :
( ( ( a @ ( A @ mult ) @ i )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( ( A @ i )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[936]) ).
thf(71,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( unit @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,15]) ).
thf(129,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( unit != a ) ),
inference(simp,[status(thm)],[71]) ).
thf(12856,plain,
( ( b != a )
| ( ( a @ i )
!= unit ) ),
inference(simp,[status(thm)],[12849]) ).
thf(12882,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( a @ i ) )
| ( b != a )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[11079,12856]) ).
thf(12897,plain,
( ( ( unit @ ( unit @ rd ) )
!= a )
| ( b != a ) ),
inference(simp,[status(thm)],[12882]) ).
thf(12999,plain,
( ( ( unit @ i )
!= a )
| ( b != a ) ),
inference(rewrite,[status(thm)],[12897,802]) ).
thf(633,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( D @ ( C @ ld ) @ ( C @ mult ) ) )
| ( A = D ) ),
inference(paramod_ordered,[status(thm)],[21,17]) ).
thf(700,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ld ) ) )
| ( ( B @ ( A @ rd ) )
!= C )
| ( A = D ) ),
inference(simp,[status(thm)],[633]) ).
thf(750,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ rd ) @ ld ) )
!= B )
| ( A = C ) ),
inference(simp,[status(thm)],[700]) ).
thf(94420,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ rd ) @ ( C @ i @ mult ) @ i )
!= B )
| ( A = C ) ),
inference(rewrite,[status(thm)],[750,2318]) ).
thf(106046,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ rd ) )
!= ( D @ ( C @ rd ) ) )
| ( ( unit @ i @ ( B @ i @ mult ) @ i )
!= D )
| ( B = C ) ),
inference(paramod_ordered,[status(thm)],[105947,78606]) ).
thf(106047,plain,
! [B: $i,A: $i] :
( ( ( unit @ i @ ( B @ i @ mult ) @ i )
!= A )
| ( B = A ) ),
inference(pattern_uni,[status(thm)],[106046:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( A ))]]) ).
thf(106351,plain,
! [A: $i] :
( ( unit @ i @ ( A @ i @ mult ) @ i )
= A ),
inference(simp,[status(thm)],[106047]) ).
thf(108532,plain,
! [A: $i] :
( ( unit @ ( A @ i @ mult ) @ i )
= A ),
inference(rewrite,[status(thm)],[106351,43]) ).
thf(46865,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( a @ ( C @ mult ) ) )
| ( A
!= ( C @ ( b @ rd ) @ i ) ) ),
inference(paramod_ordered,[status(thm)],[21,32795]) ).
thf(46866,plain,
! [A: $i] :
( ( a @ ( A @ rd ) @ ( b @ rd ) @ i )
!= A ),
inference(pattern_uni,[status(thm)],[46865:[bind(A,$thf( D )),bind(B,$thf( a )),bind(C,$thf( a @ ( D @ rd ) ))]]) ).
thf(46948,plain,
! [A: $i] :
( ( a @ ( A @ rd ) @ ( b @ rd ) @ i )
!= A ),
inference(simp,[status(thm)],[46866]) ).
thf(65200,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ rd ) @ i )
!= ( a @ ( C @ rd ) @ ( b @ rd ) @ i ) )
| ( ( A @ i @ ( B @ mult ) )
!= C ) ),
inference(paramod_ordered,[status(thm)],[975,46948]) ).
thf(65201,plain,
! [A: $i] :
( ( b @ i @ ( a @ ( A @ rd ) @ mult ) )
!= A ),
inference(pattern_uni,[status(thm)],[65200:[bind(A,$thf( b )),bind(B,$thf( a @ ( D @ rd ) )),bind(C,$thf( D ))]]) ).
thf(65310,plain,
! [A: $i] :
( ( b @ i @ ( a @ ( A @ rd ) @ mult ) )
!= A ),
inference(simp,[status(thm)],[65201]) ).
thf(48559,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ rd ) @ i )
!= ( B @ i ) )
| ( ( unit @ ( B @ ( unit @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[3288,48409]) ).
thf(48560,plain,
! [A: $i] :
( ( unit @ ( A @ ( A @ rd ) @ ( unit @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48559:[bind(A,$thf( D )),bind(B,$thf( D @ ( D @ rd ) ))]]) ).
thf(48707,plain,
! [A: $i] :
( ( unit @ ( A @ ( A @ rd ) @ ( unit @ mult ) @ rd ) )
= unit ),
inference(simp,[status(thm)],[48560]) ).
thf(90704,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ ( unit @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48707,713]) ).
thf(90766,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ rd ) @ ( unit @ mult ) )
!= ( B @ ( C @ mult ) ) )
| ( ( unit @ i @ ( B @ mult ) )
= ( C @ i ) ) ),
inference(paramod_ordered,[status(thm)],[90704,29]) ).
thf(90767,plain,
! [A: $i] :
( ( unit @ i @ ( A @ ( A @ rd ) @ mult ) )
= ( unit @ i ) ),
inference(pattern_uni,[status(thm)],[90766:[bind(A,$thf( E )),bind(B,$thf( E @ ( E @ rd ) )),bind(C,$thf( unit ))]]) ).
thf(92473,plain,
! [A: $i] :
( ( unit @ i @ ( A @ ( A @ rd ) @ mult ) )
= ( unit @ i ) ),
inference(simp,[status(thm)],[90767]) ).
thf(95525,plain,
! [A: $i] :
( ( unit @ ( A @ ( A @ rd ) @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[92473,43]) ).
thf(24892,plain,
! [B: $i,A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( b @ ( B @ i @ rd ) @ ( B @ mult ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[25,11074]) ).
thf(24946,plain,
! [A: $i] :
( ( ( b @ ( A @ i @ rd ) )
!= unit )
| ( a != A ) ),
inference(simp,[status(thm)],[24892]) ).
thf(24970,plain,
( ( b @ ( a @ i @ rd ) )
!= unit ),
inference(simp,[status(thm)],[24946]) ).
thf(25011,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( b @ ( a @ i @ rd ) ) )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[1829,24970]) ).
thf(25022,plain,
( ( b @ ( a @ i @ rd ) )
!= ( unit @ i @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[25011]) ).
thf(25201,plain,
( ( b @ ( a @ i @ rd ) )
!= ( unit @ i @ i ) ),
inference(rewrite,[status(thm)],[25022,802]) ).
thf(25227,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( b @ ( a @ i @ rd ) ) )
| ( A
!= ( unit @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1829,25201]) ).
thf(25261,plain,
( ( b @ ( a @ i @ rd ) )
!= ( unit @ i @ i @ i @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[25227]) ).
thf(26325,plain,
( ( b @ ( a @ i @ rd ) )
!= ( unit @ i @ i @ i @ i ) ),
inference(rewrite,[status(thm)],[25261,802]) ).
thf(40358,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( b @ ( A @ rd ) @ ( unit @ mult ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[22781,24962]) ).
thf(40359,plain,
( ( b @ ( unit @ i @ i @ i @ i @ i @ rd ) @ ( unit @ mult ) )
!= a ),
inference(pattern_uni,[status(thm)],[40358:[bind(A,$thf( unit @ i @ i @ i @ i @ i ))]]) ).
thf(41590,plain,
( ( b @ ( unit @ i @ i @ i @ i @ i @ rd ) )
!= a ),
inference(rewrite,[status(thm)],[40359,27]) ).
thf(38074,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ ( unit @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[22781,14259]) ).
thf(38075,plain,
( ( unit @ i @ i @ i @ i @ i @ ( unit @ mult ) )
!= ( b @ ( a @ mult ) ) ),
inference(pattern_uni,[status(thm)],[38074:[bind(A,$thf( unit @ i @ i @ i @ i @ i ))]]) ).
thf(39618,plain,
( ( b @ ( a @ mult ) )
!= ( unit @ i @ i @ i @ i @ i ) ),
inference(rewrite,[status(thm)],[38075,27]) ).
thf(40376,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i )
!= ( A @ i ) )
| ( ( b @ ( A @ rd ) @ ( unit @ mult ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[20919,24962]) ).
thf(40377,plain,
( ( b @ ( unit @ i @ i @ rd ) @ ( unit @ mult ) )
!= a ),
inference(pattern_uni,[status(thm)],[40376:[bind(A,$thf( unit @ i @ i ))]]) ).
thf(40452,plain,
( ( b @ ( unit @ i @ i @ rd ) )
!= a ),
inference(rewrite,[status(thm)],[40377,27]) ).
thf(12830,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( b @ i ) )
| ( A != unit )
| ( ( a @ i )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[11079,11917]) ).
thf(12874,plain,
( ( ( unit @ ( unit @ rd ) )
!= b )
| ( ( a @ i )
!= unit ) ),
inference(simp,[status(thm)],[12830]) ).
thf(15344,plain,
( ( ( unit @ i )
!= b )
| ( ( a @ i )
!= unit ) ),
inference(rewrite,[status(thm)],[12874,802]) ).
thf(662,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( A @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[645]) ).
thf(12888,plain,
! [A: $i] :
( ( ( A @ ( A @ rd ) @ i )
!= ( a @ i ) )
| ( b != a )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[3288,12856]) ).
thf(12889,plain,
! [A: $i] :
( ( ( A @ ( A @ rd ) @ i )
!= ( a @ i ) )
| ( b != a ) ),
inference(simp,[status(thm)],[12888]) ).
thf(12902,plain,
! [A: $i] :
( ( ( A @ ( A @ rd ) )
!= a )
| ( b != a ) ),
inference(simp,[status(thm)],[12889]) ).
thf(26648,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( a @ ( unit @ i @ rd ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[1829,26620]) ).
thf(26674,plain,
( ( a @ ( unit @ i @ rd ) )
!= ( b @ i @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[26648]) ).
thf(27859,plain,
( ( a @ ( unit @ rd ) )
!= ( b @ i @ i ) ),
inference(rewrite,[status(thm)],[26674,802,43]) ).
thf(81001,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ rd ) )
!= ( B @ ( B @ rd ) ) )
| ( ( A @ i @ ( a @ rd ) )
!= ( b @ i ) ) ),
inference(paramod_ordered,[status(thm)],[802,75176]) ).
thf(81002,plain,
( ( unit @ i @ ( a @ rd ) )
!= ( b @ i ) ),
inference(pattern_uni,[status(thm)],[81001:[bind(A,$thf( unit )),bind(B,$thf( unit ))]]) ).
thf(81078,plain,
( ( unit @ ( a @ rd ) )
!= ( b @ i ) ),
inference(rewrite,[status(thm)],[81002,43]) ).
thf(25360,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( b @ i @ ( a @ rd ) ) )
| ( A
!= ( unit @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1829,25334]) ).
thf(25377,plain,
( ( unit @ i @ i @ i @ ( unit @ rd ) )
!= ( b @ i @ ( a @ rd ) ) ),
inference(simp,[status(thm)],[25360]) ).
thf(26402,plain,
( ( b @ i @ ( a @ rd ) )
!= ( unit @ i @ i @ i @ i ) ),
inference(rewrite,[status(thm)],[25377,802]) ).
thf(81014,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( C @ ( C @ rd ) @ ( a @ rd ) ) )
| ( A
!= ( b @ i ) ) ),
inference(paramod_ordered,[status(thm)],[23,75176]) ).
thf(81035,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( B @ rd ) ) )
| ( ( A @ ( b @ i @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[81014]) ).
thf(81059,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ ( b @ i @ mult ) )
!= a ),
inference(simp,[status(thm)],[81035]) ).
thf(578,plain,
! [C: $i,B: $i,A: $i] :
( ( ( unit @ ( A @ ld ) )
!= ( C @ ( B @ mult ) @ ( B @ ld ) ) )
| ( ( A @ i )
= C ) ),
inference(paramod_ordered,[status(thm)],[532,19]) ).
thf(584,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ mult ) )
!= unit )
| ( A != B )
| ( ( A @ i )
= C ) ),
inference(simp,[status(thm)],[578]) ).
thf(586,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ mult ) )
!= unit )
| ( ( A @ i )
= B ) ),
inference(simp,[status(thm)],[584]) ).
thf(19947,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ rd ) @ i )
!= ( B @ i ) )
| ( ( unit @ i @ ( B @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[3288,19879]) ).
thf(19948,plain,
! [A: $i] :
( ( unit @ i @ ( A @ ( A @ rd ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[19947:[bind(A,$thf( D )),bind(B,$thf( D @ ( D @ rd ) ))]]) ).
thf(20031,plain,
! [A: $i] :
( ( unit @ i @ ( A @ ( A @ rd ) @ rd ) )
= unit ),
inference(simp,[status(thm)],[19948]) ).
thf(38809,plain,
! [A: $i] :
( ( unit @ ( A @ ( A @ rd ) @ rd ) )
= unit ),
inference(rewrite,[status(thm)],[20031,43]) ).
thf(95409,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ ( b @ rd ) @ ( unit @ rd ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[22320,86342]) ).
thf(95410,plain,
( ( unit @ i @ i @ i @ i @ ( b @ rd ) @ ( unit @ rd ) )
!= a ),
inference(pattern_uni,[status(thm)],[95409:[bind(A,$thf( unit @ i @ i @ i @ i ))]]) ).
thf(98296,plain,
( ( unit @ i @ i @ i @ i @ ( b @ rd ) @ i )
!= a ),
inference(rewrite,[status(thm)],[95410,802]) ).
thf(59,plain,
! [A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( a @ ( b @ mult ) ) )
| ( ( c @ ( a @ ( A @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,15]) ).
thf(100,plain,
! [A: $i] :
( ( unit != a )
| ( A != b )
| ( ( c @ ( a @ ( A @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[59]) ).
thf(166,plain,
( ( unit != a )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( b @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[100]) ).
thf(48333,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ ( unit @ mult ) )
!= ( a @ ( b @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21498,45987]) ).
thf(48334,plain,
( ( unit @ i @ i @ i @ ( unit @ mult ) )
!= ( a @ ( b @ mult ) ) ),
inference(pattern_uni,[status(thm)],[48333:[bind(A,$thf( unit @ i @ i @ i ))]]) ).
thf(53931,plain,
( ( a @ ( b @ mult ) )
!= ( unit @ i @ i @ i ) ),
inference(rewrite,[status(thm)],[48334,27]) ).
thf(46349,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( C @ ( C @ rd ) ) )
| ( A
!= ( a @ ( b @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,46010]) ).
thf(46358,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ ( a @ ( b @ mult ) @ mult ) )
!= B ) ),
inference(simp,[status(thm)],[46349]) ).
thf(46367,plain,
! [A: $i] :
( ( A @ ( a @ ( b @ mult ) @ mult ) )
!= A ),
inference(simp,[status(thm)],[46358]) ).
thf(6993,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( unit @ i @ mult ) )
!= ( B @ i @ ( C @ mult ) ) )
| ( A
= ( C @ ( B @ rd ) @ i ) ) ),
inference(paramod_ordered,[status(thm)],[6930,975]) ).
thf(6994,plain,
! [A: $i] :
( ( unit @ i @ ( A @ rd ) @ i )
= ( A @ i ) ),
inference(pattern_uni,[status(thm)],[6993:[bind(A,$thf( E @ i )),bind(B,$thf( E )),bind(C,$thf( unit @ i ))]]) ).
thf(7319,plain,
! [A: $i] :
( ( unit @ i @ ( A @ rd ) @ i )
= ( A @ i ) ),
inference(simp,[status(thm)],[6994]) ).
thf(8728,plain,
! [A: $i] :
( ( unit @ ( A @ rd ) @ i )
= ( A @ i ) ),
inference(rewrite,[status(thm)],[7319,43]) ).
thf(308,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( B @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,15]) ).
thf(321,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( B @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[308]) ).
thf(26768,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( B @ mult ) )
!= a ) ),
inference(rewrite,[status(thm)],[321,2318]) ).
thf(38091,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ ( unit @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[20919,14259]) ).
thf(38092,plain,
( ( unit @ i @ i @ ( unit @ mult ) )
!= ( b @ ( a @ mult ) ) ),
inference(pattern_uni,[status(thm)],[38091:[bind(A,$thf( unit @ i @ i ))]]) ).
thf(38146,plain,
( ( b @ ( a @ mult ) )
!= ( unit @ i @ i ) ),
inference(rewrite,[status(thm)],[38092,27]) ).
thf(55,plain,
! [A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,15]) ).
thf(116,plain,
! [A: $i] :
( ( unit != a )
| ( A
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[55]) ).
thf(180,plain,
( ( unit != a )
| ( ( c @ ( a @ mult ) @ ( b @ ( a @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[116]) ).
thf(3676,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( C @ ( C @ rd ) ) )
| ( A != b )
| ( unit != a ) ),
inference(paramod_ordered,[status(thm)],[23,3649]) ).
thf(3687,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ ( b @ mult ) )
!= B )
| ( unit != a ) ),
inference(simp,[status(thm)],[3676]) ).
thf(3696,plain,
! [A: $i] :
( ( ( A @ ( b @ mult ) )
!= A )
| ( unit != a ) ),
inference(simp,[status(thm)],[3687]) ).
thf(58,plain,
! [A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( A @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,15]) ).
thf(136,plain,
! [A: $i] :
( ( unit != c )
| ( A != a )
| ( ( A @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[58]) ).
thf(149,plain,
( ( unit != c )
| ( ( a @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[136]) ).
thf(130,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ i )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( unit @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[71]) ).
thf(144,plain,
( ( ( b @ ( a @ mult ) )
!= ( a @ i ) )
| ( ( c @ ( a @ mult ) @ ( unit @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[130]) ).
thf(11920,plain,
( ( ( b @ ( a @ mult ) )
!= ( a @ i ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[144,27]) ).
thf(10,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ mult ) @ mult ) )
= ( C @ ( B @ mult ) @ ( C @ ld ) @ ( C @ ( A @ mult ) @ mult ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c09) ).
thf(32,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ mult ) @ mult ) )
= ( C @ ( B @ mult ) @ ( C @ ld ) @ ( C @ ( A @ mult ) @ mult ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(32730,plain,
( ( ( a @ ( unit @ i @ rd ) )
!= unit )
| ( unit != b ) ),
inference(simp,[status(thm)],[32723]) ).
thf(33587,plain,
( ( ( a @ ( unit @ rd ) )
!= unit )
| ( unit != b ) ),
inference(rewrite,[status(thm)],[32730,43]) ).
thf(1764,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( C @ ( B @ mult ) ) )
| ( ( unit @ i @ ( B @ i @ rd ) )
= C ) ),
inference(paramod_ordered,[status(thm)],[37,972]) ).
thf(1765,plain,
! [A: $i] :
( ( unit @ i @ ( A @ i @ rd ) )
= ( A @ i ) ),
inference(pattern_uni,[status(thm)],[1764:[bind(A,$thf( D )),bind(B,$thf( D )),bind(C,$thf( D @ i ))]]) ).
thf(1818,plain,
! [A: $i] :
( ( unit @ i @ ( A @ i @ rd ) )
= ( A @ i ) ),
inference(simp,[status(thm)],[1765]) ).
thf(1884,plain,
! [A: $i] :
( ( unit @ ( A @ i @ rd ) )
= ( A @ i ) ),
inference(rewrite,[status(thm)],[1818,43]) ).
thf(693,plain,
! [B: $i,A: $i] :
( ( B != a )
| ( ( B @ ( A @ rd ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[644]) ).
thf(743,plain,
! [A: $i] :
( ( ( a @ ( A @ rd ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[693]) ).
thf(408,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( C @ i @ ( C @ mult ) ) )
| ( B = unit ) ),
inference(paramod_ordered,[status(thm)],[17,37]) ).
thf(440,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= ( C @ i ) )
| ( A != C )
| ( B = unit ) ),
inference(simp,[status(thm)],[408]) ).
thf(501,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ld ) )
!= ( B @ i ) )
| ( A = unit ) ),
inference(simp,[status(thm)],[440]) ).
thf(67316,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ i @ mult ) @ i )
!= ( B @ i ) )
| ( A = unit ) ),
inference(rewrite,[status(thm)],[501,2318]) ).
thf(26529,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( a @ ( C @ rd ) @ ( C @ i @ mult ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[21,11766]) ).
thf(26579,plain,
! [B: $i,A: $i] :
( ( A
!= ( a @ ( B @ rd ) ) )
| ( ( A @ ( b @ rd ) )
!= ( B @ i ) ) ),
inference(simp,[status(thm)],[26529]) ).
thf(26604,plain,
! [A: $i] :
( ( a @ ( A @ rd ) @ ( b @ rd ) )
!= ( A @ i ) ),
inference(simp,[status(thm)],[26579]) ).
thf(1754,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( D @ ( C @ mult ) ) )
| ( ( B @ i @ ( C @ i @ rd ) )
= D ) ),
inference(paramod_ordered,[status(thm)],[17,972]) ).
thf(1755,plain,
! [B: $i,A: $i] :
( ( B @ i @ ( A @ i @ rd ) )
= ( B @ ( A @ ld ) ) ),
inference(pattern_uni,[status(thm)],[1754:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( E )),bind(D,$thf( F @ ( E @ ld ) ))]]) ).
thf(1816,plain,
! [B: $i,A: $i] :
( ( B @ i @ ( A @ i @ rd ) )
= ( B @ ( A @ ld ) ) ),
inference(simp,[status(thm)],[1755]) ).
thf(5390,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ i @ ( A @ i @ rd ) )
!= ( C @ ( C @ rd ) ) )
| ( ( B @ ( A @ ld ) @ i )
= unit ) ),
inference(paramod_ordered,[status(thm)],[1816,3288]) ).
thf(5391,plain,
! [A: $i] :
( ( A @ ( A @ ld ) @ i )
= unit ),
inference(pattern_uni,[status(thm)],[5390:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B @ i ))]]) ).
thf(5416,plain,
! [A: $i] :
( ( A @ ( A @ ld ) @ i )
= unit ),
inference(simp,[status(thm)],[5391]) ).
thf(12883,plain,
! [A: $i] :
( ( ( A @ ( A @ ld ) @ i )
!= ( a @ i ) )
| ( b != a )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[5416,12856]) ).
thf(12884,plain,
! [A: $i] :
( ( ( A @ ( A @ ld ) @ i )
!= ( a @ i ) )
| ( b != a ) ),
inference(simp,[status(thm)],[12883]) ).
thf(12892,plain,
! [A: $i] :
( ( ( A @ ( A @ ld ) )
!= a )
| ( b != a ) ),
inference(simp,[status(thm)],[12884]) ).
thf(18548,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) @ i )
!= a )
| ( b != a ) ),
inference(rewrite,[status(thm)],[12892,2318]) ).
thf(48437,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( unit @ ( A @ ( unit @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[22320,48409]) ).
thf(48438,plain,
( ( unit @ ( unit @ i @ i @ i @ i @ ( unit @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48437:[bind(A,$thf( unit @ i @ i @ i @ i ))]]) ).
thf(55661,plain,
( ( unit @ i @ i @ i @ i @ ( unit @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48438,713]) ).
thf(536,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ ld ) )
!= ( C @ ( B @ mult ) @ ( B @ ld ) ) )
| ( unit = C ) ),
inference(paramod_ordered,[status(thm)],[525,19]) ).
thf(543,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ mult ) ) )
| ( A != B )
| ( unit = C ) ),
inference(simp,[status(thm)],[536]) ).
thf(545,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ mult ) )
!= A )
| ( unit = B ) ),
inference(simp,[status(thm)],[543]) ).
thf(82,plain,
! [A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( A @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[56]) ).
thf(2859,plain,
! [A: $i] :
( ( A
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( A @ mult ) )
!= a ) ),
inference(rewrite,[status(thm)],[82,25]) ).
thf(48552,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( unit @ ( A @ ( unit @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[28857,48409]) ).
thf(48553,plain,
( ( unit @ ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ ( unit @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48552:[bind(A,$thf( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i ))]]) ).
thf(68904,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ ( unit @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48553,713]) ).
thf(11800,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( a @ ( unit @ rd ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[23,11792]) ).
thf(11811,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ ( b @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[11800]) ).
thf(11819,plain,
( ( a @ ( b @ mult ) )
!= unit ),
inference(simp,[status(thm)],[11811]) ).
thf(5380,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ i @ ( A @ i @ rd ) )
!= ( C @ ( C @ rd ) ) )
| ( ( B @ ( A @ ld ) )
!= a )
| ( unit != b ) ),
inference(paramod_ordered,[status(thm)],[1816,3652]) ).
thf(5381,plain,
! [A: $i] :
( ( ( A @ ( A @ ld ) )
!= a )
| ( unit != b ) ),
inference(pattern_uni,[status(thm)],[5380:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B @ i ))]]) ).
thf(5412,plain,
! [A: $i] :
( ( ( A @ ( A @ ld ) )
!= a )
| ( unit != b ) ),
inference(simp,[status(thm)],[5381]) ).
thf(5558,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ mult ) @ ( A @ ld ) )
!= ( C @ ( C @ ld ) ) )
| ( B != a )
| ( unit != b ) ),
inference(paramod_ordered,[status(thm)],[19,5412]) ).
thf(5562,plain,
! [B: $i,A: $i] :
( ( ( a @ ( A @ mult ) )
!= B )
| ( A != B )
| ( unit != b ) ),
inference(simp,[status(thm)],[5558]) ).
thf(5567,plain,
! [A: $i] :
( ( ( a @ ( A @ mult ) )
!= A )
| ( unit != b ) ),
inference(simp,[status(thm)],[5562]) ).
thf(106116,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ rd ) )
!= ( B @ ( b @ rd ) ) )
| ( ( unit @ i @ ( B @ i @ rd ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[105947,86342]) ).
thf(106117,plain,
( ( unit @ i @ ( b @ i @ rd ) )
!= a ),
inference(pattern_uni,[status(thm)],[106116:[bind(A,$thf( b )),bind(B,$thf( b ))]]) ).
thf(107534,plain,
( ( unit @ ( b @ i @ rd ) )
!= a ),
inference(rewrite,[status(thm)],[106117,43]) ).
thf(41878,plain,
! [A: $i] :
( ( ( unit @ ( unit @ rd ) )
!= ( A @ ( a @ rd ) ) )
| ( ( b @ ( unit @ i @ rd ) )
!= A ) ),
inference(paramod_ordered,[status(thm)],[21387,24968]) ).
thf(41888,plain,
( ( ( b @ ( unit @ i @ rd ) )
!= unit )
| ( unit != a ) ),
inference(simp,[status(thm)],[41878]) ).
thf(42215,plain,
( ( ( b @ ( unit @ rd ) )
!= unit )
| ( unit != a ) ),
inference(rewrite,[status(thm)],[41888,43]) ).
thf(76490,plain,
( ( unit @ ( unit @ mult ) )
!= ( unit @ i @ ( b @ rd ) @ ( a @ mult ) ) ),
inference(simp,[status(thm)],[76468]) ).
thf(77505,plain,
( ( unit @ ( b @ rd ) @ ( a @ mult ) )
!= unit ),
inference(rewrite,[status(thm)],[76490,43,48733]) ).
thf(3684,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( B @ ( B @ rd ) ) )
| ( A != b )
| ( unit != a ) ),
inference(paramod_ordered,[status(thm)],[1829,3649]) ).
thf(3691,plain,
! [A: $i] :
( ( ( b @ i )
!= A )
| ( unit != A )
| ( unit != a ) ),
inference(simp,[status(thm)],[3684]) ).
thf(3700,plain,
( ( ( b @ i )
!= unit )
| ( unit != a ) ),
inference(simp,[status(thm)],[3691]) ).
thf(22696,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
!= ( a @ i @ ( b @ rd ) ) )
| ( A
!= ( unit @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1825,22686]) ).
thf(22729,plain,
! [A: $i] :
( ( ( unit @ i @ i @ ( A @ i @ mult ) @ i )
!= ( a @ i ) )
| ( A != b ) ),
inference(simp,[status(thm)],[22696]) ).
thf(22745,plain,
( ( unit @ i @ i @ ( b @ i @ mult ) @ i )
!= ( a @ i ) ),
inference(simp,[status(thm)],[22729]) ).
thf(23202,plain,
( ( unit @ ( b @ i @ mult ) @ i )
!= ( a @ i ) ),
inference(rewrite,[status(thm)],[22745,20045]) ).
thf(23240,plain,
( ( ( unit @ i )
!= ( b @ i ) )
| ( ( unit @ ( unit @ mult ) @ i )
!= ( a @ i ) ) ),
inference(paramod_ordered,[status(thm)],[43,23202]) ).
thf(23274,plain,
( ( unit != b )
| ( ( unit @ ( unit @ mult ) @ i )
!= ( a @ i ) ) ),
inference(simp,[status(thm)],[23240]) ).
thf(44823,plain,
( ( unit != b )
| ( ( unit @ i )
!= ( a @ i ) ) ),
inference(rewrite,[status(thm)],[23274,7904]) ).
thf(84972,plain,
( ( unit @ ( unit @ mult ) )
!= ( unit @ i @ ( a @ rd ) @ ( b @ mult ) ) ),
inference(simp,[status(thm)],[84947]) ).
thf(85860,plain,
( ( unit @ ( a @ rd ) @ ( b @ mult ) )
!= unit ),
inference(rewrite,[status(thm)],[84972,43,48733]) ).
thf(74311,plain,
! [A: $i] :
( ( ( A @ ( A @ ( b @ rd ) @ mult ) )
!= ( unit @ i @ ( unit @ mult ) ) )
| ( ( a @ i )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[50298,68461]) ).
thf(74331,plain,
! [A: $i] :
( ( A
!= ( unit @ i ) )
| ( ( A @ ( b @ rd ) )
!= unit )
| ( ( a @ i )
!= unit ) ),
inference(simp,[status(thm)],[74311]) ).
thf(74361,plain,
( ( ( unit @ i @ ( b @ rd ) )
!= unit )
| ( ( a @ i )
!= unit ) ),
inference(simp,[status(thm)],[74331]) ).
thf(105491,plain,
( ( ( unit @ ( b @ rd ) )
!= unit )
| ( ( a @ i )
!= unit ) ),
inference(rewrite,[status(thm)],[74361,43]) ).
thf(60,plain,
! [A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) )
| ( A
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,15]) ).
thf(86,plain,
( ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= unit )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[60]) ).
thf(70,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( ( A @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,15]) ).
thf(88,plain,
! [A: $i] :
( ( A != c )
| ( ( a @ ( a @ ( b @ mult ) @ mult ) )
!= unit )
| ( ( A @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[70]) ).
thf(159,plain,
( ( ( a @ ( a @ ( b @ mult ) @ mult ) )
!= unit )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[88]) ).
thf(5353,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ i @ ( A @ i @ rd ) )
!= ( C @ ( C @ rd ) ) )
| ( ( B @ ( A @ ld ) )
!= b )
| ( unit != a ) ),
inference(paramod_ordered,[status(thm)],[1816,3649]) ).
thf(5354,plain,
! [A: $i] :
( ( ( A @ ( A @ ld ) )
!= b )
| ( unit != a ) ),
inference(pattern_uni,[status(thm)],[5353:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B @ i ))]]) ).
thf(5428,plain,
! [A: $i] :
( ( ( A @ ( A @ ld ) )
!= b )
| ( unit != a ) ),
inference(simp,[status(thm)],[5354]) ).
thf(6039,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ mult ) @ ( A @ ld ) )
!= ( C @ ( C @ ld ) ) )
| ( B != b )
| ( unit != a ) ),
inference(paramod_ordered,[status(thm)],[19,5428]) ).
thf(6043,plain,
! [B: $i,A: $i] :
( ( ( b @ ( A @ mult ) )
!= B )
| ( A != B )
| ( unit != a ) ),
inference(simp,[status(thm)],[6039]) ).
thf(6048,plain,
! [A: $i] :
( ( ( b @ ( A @ mult ) )
!= A )
| ( unit != a ) ),
inference(simp,[status(thm)],[6043]) ).
thf(649,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) )
| ( A
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,15]) ).
thf(685,plain,
! [A: $i] :
( ( A
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( ( A @ ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) @ rd ) )
!= a ) ),
inference(simp,[status(thm)],[649]) ).
thf(736,plain,
( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) @ rd ) )
!= a ),
inference(simp,[status(thm)],[685]) ).
thf(81083,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
!= ( unit @ ( a @ rd ) ) )
| ( A
!= ( b @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1825,81078]) ).
thf(81103,plain,
! [A: $i] :
( ( ( b @ i @ ( A @ i @ mult ) @ i )
!= unit )
| ( A != a ) ),
inference(simp,[status(thm)],[81083]) ).
thf(81117,plain,
( ( b @ i @ ( a @ i @ mult ) @ i )
!= unit ),
inference(simp,[status(thm)],[81103]) ).
thf(648,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( a @ ( b @ mult ) ) )
| ( ( c @ ( a @ ( A @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,15]) ).
thf(687,plain,
! [B: $i,A: $i] :
( ( B != a )
| ( ( B @ ( A @ rd ) )
!= b )
| ( ( c @ ( a @ ( A @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[648]) ).
thf(737,plain,
! [A: $i] :
( ( ( a @ ( A @ rd ) )
!= b )
| ( ( c @ ( a @ ( A @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[687]) ).
thf(13031,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A
!= ( unit @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1825,13024]) ).
thf(13066,plain,
! [A: $i] :
( ( ( unit @ i @ ( A @ i @ mult ) @ i )
!= a )
| ( A
!= ( b @ i ) ) ),
inference(simp,[status(thm)],[13031]) ).
thf(13078,plain,
( ( unit @ i @ ( b @ i @ i @ mult ) @ i )
!= a ),
inference(simp,[status(thm)],[13066]) ).
thf(15453,plain,
( ( unit @ ( b @ mult ) @ i )
!= a ),
inference(rewrite,[status(thm)],[13078,43,571]) ).
thf(11877,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[1825,11780]) ).
thf(11901,plain,
! [A: $i] :
( ( ( unit @ ( A @ i @ mult ) @ i )
!= a )
| ( A
!= ( b @ i ) ) ),
inference(simp,[status(thm)],[11877]) ).
thf(11919,plain,
( ( unit @ ( b @ i @ i @ mult ) @ i )
!= a ),
inference(simp,[status(thm)],[11901]) ).
thf(14042,plain,
( ( b @ i @ i @ i )
!= a ),
inference(rewrite,[status(thm)],[11919,7904]) ).
thf(908,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( ( B @ i @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,15]) ).
thf(945,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= c )
| ( A
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( B @ i @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[908]) ).
thf(990,plain,
! [A: $i] :
( ( ( a @ ( a @ ( b @ mult ) @ mult ) @ ( A @ mult ) @ i )
!= c )
| ( ( A @ i @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[945]) ).
thf(893,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( B @ ( C @ mult ) @ i @ ( B @ mult ) ) )
| ( ( C @ i )
= unit ) ),
inference(paramod_ordered,[status(thm)],[35,29]) ).
thf(951,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( B @ ( C @ mult ) @ i ) )
| ( ( A @ i )
!= B )
| ( ( C @ i )
= unit ) ),
inference(simp,[status(thm)],[893]) ).
thf(996,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ ( B @ mult ) @ i )
!= A )
| ( ( B @ i )
= unit ) ),
inference(simp,[status(thm)],[951]) ).
thf(44825,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( unit @ i ) )
| ( unit != b )
| ( A
!= ( a @ i ) ) ),
inference(paramod_ordered,[status(thm)],[11079,44823]) ).
thf(44862,plain,
( ( ( a @ i @ ( unit @ rd ) )
!= unit )
| ( unit != b ) ),
inference(simp,[status(thm)],[44825]) ).
thf(45377,plain,
( ( ( a @ i @ i )
!= unit )
| ( unit != b ) ),
inference(rewrite,[status(thm)],[44862,802]) ).
thf(47855,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( b @ ( a @ i @ ( C @ mult ) @ rd ) ) )
| ( A != C ) ),
inference(paramod_ordered,[status(thm)],[23,41953]) ).
thf(47892,plain,
! [B: $i,A: $i] :
( ( A != b )
| ( ( A @ ( B @ mult ) )
!= ( a @ i @ ( B @ mult ) ) ) ),
inference(simp,[status(thm)],[47855]) ).
thf(47919,plain,
! [A: $i] :
( ( a @ i @ ( A @ mult ) )
!= ( b @ ( A @ mult ) ) ),
inference(simp,[status(thm)],[47892]) ).
thf(305,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( C @ ( B @ ld ) @ ( B @ mult ) ) )
| ( unit = C ) ),
inference(paramod_ordered,[status(thm)],[35,17]) ).
thf(351,plain,
! [C: $i,B: $i,A: $i] :
( ( A
!= ( C @ ( B @ ld ) ) )
| ( ( A @ i )
!= B )
| ( unit = C ) ),
inference(simp,[status(thm)],[305]) ).
thf(389,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ i @ ld ) )
!= A )
| ( unit = B ) ),
inference(simp,[status(thm)],[351]) ).
thf(43498,plain,
! [B: $i,A: $i] :
( ( ( A @ i @ ( B @ i @ mult ) @ i )
!= A )
| ( unit = B ) ),
inference(rewrite,[status(thm)],[389,2318]) ).
thf(468,plain,
! [A: $i] :
( ( ( A @ i )
!= a )
| ( A
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( unit != a ) ),
inference(simp,[status(thm)],[425]) ).
thf(494,plain,
( ( ( b @ ( a @ mult ) @ i )
!= a )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( unit != a ) ),
inference(simp,[status(thm)],[468]) ).
thf(407,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( C @ ( B @ ld ) @ ( B @ mult ) ) )
| ( unit = C ) ),
inference(paramod_ordered,[status(thm)],[37,17]) ).
thf(462,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i )
!= ( C @ ( B @ ld ) ) )
| ( A != B )
| ( unit = C ) ),
inference(simp,[status(thm)],[407]) ).
thf(490,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= ( A @ i ) )
| ( unit = B ) ),
inference(simp,[status(thm)],[462]) ).
thf(53761,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i )
!= ( A @ i ) )
| ( unit = B ) ),
inference(rewrite,[status(thm)],[490,2318]) ).
thf(16351,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A
!= ( unit @ i @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1829,16335]) ).
thf(16356,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i @ i @ i @ i @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[16351]) ).
thf(18387,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i @ i @ i @ i @ i ) ),
inference(rewrite,[status(thm)],[16356,802]) ).
thf(18388,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( ( A @ i )
!= ( unit @ i @ i @ i @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[802,18387]) ).
thf(18406,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A
!= ( unit @ i @ i @ i @ i ) ) ),
inference(simp,[status(thm)],[18388]) ).
thf(18430,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i @ i @ i @ i @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[18406]) ).
thf(20699,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i @ i @ i @ i @ i ) ),
inference(rewrite,[status(thm)],[18430,802]) ).
thf(20700,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( ( A @ i )
!= ( unit @ i @ i @ i @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[802,20699]) ).
thf(20743,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) )
!= ( a @ ( b @ i @ rd ) ) )
| ( A
!= ( unit @ i @ i @ i @ i ) ) ),
inference(simp,[status(thm)],[20700]) ).
thf(20749,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i @ i @ i @ i @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[20743]) ).
thf(24193,plain,
( ( a @ ( b @ i @ rd ) )
!= ( unit @ i @ i @ i @ i @ i ) ),
inference(rewrite,[status(thm)],[20749,802]) ).
thf(355,plain,
! [A: $i] :
( ( ( unit @ ( A @ ld ) @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[318]) ).
thf(30925,plain,
! [A: $i] :
( ( ( A @ ( unit @ i @ mult ) @ i @ ( A @ mult ) )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[355,2318]) ).
thf(19322,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
!= ( b @ ( unit @ rd ) ) )
| ( A
!= ( a @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1825,19318]) ).
thf(19333,plain,
! [A: $i] :
( ( ( a @ i @ i @ ( A @ i @ mult ) @ i )
!= b )
| ( A != unit ) ),
inference(simp,[status(thm)],[19322]) ).
thf(19343,plain,
( ( a @ i @ i @ ( unit @ i @ mult ) @ i )
!= b ),
inference(simp,[status(thm)],[19333]) ).
thf(19357,plain,
( ( a @ i @ i @ i )
!= b ),
inference(rewrite,[status(thm)],[19343,6930]) ).
thf(646,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) )
| ( A
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,15]) ).
thf(674,plain,
! [A: $i] :
( ( A @ ( A @ ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) @ rd ) @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ),
inference(simp,[status(thm)],[646]) ).
thf(726,plain,
! [A: $i] :
( ( A @ ( A @ ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) @ rd ) @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ),
inference(simp,[status(thm)],[674]) ).
thf(65,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) )
| ( A
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,15]) ).
thf(91,plain,
( ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( b @ ( a @ mult ) @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[65]) ).
thf(45842,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( C @ ( a @ ( C @ mult ) @ i @ mult ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[21,26591]) ).
thf(45887,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ ( b @ rd ) )
!= ( a @ ( B @ mult ) @ i ) ) ),
inference(simp,[status(thm)],[45842]) ).
thf(45930,plain,
! [A: $i] :
( ( A @ ( b @ rd ) )
!= ( a @ ( A @ mult ) @ i ) ),
inference(simp,[status(thm)],[45887]) ).
thf(466,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( unit != a ) ),
inference(simp,[status(thm)],[425]) ).
thf(46451,plain,
( ( ( a @ ( b @ ( a @ mult ) @ mult ) )
!= unit )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( unit != a ) ),
inference(rewrite,[status(thm)],[466,37]) ).
thf(47552,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( C @ ( b @ ( C @ mult ) @ i @ mult ) ) )
| ( A != a ) ),
inference(paramod_ordered,[status(thm)],[21,40421]) ).
thf(47591,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ ( a @ rd ) )
!= ( b @ ( B @ mult ) @ i ) ) ),
inference(simp,[status(thm)],[47552]) ).
thf(47632,plain,
! [A: $i] :
( ( A @ ( a @ rd ) )
!= ( b @ ( A @ mult ) @ i ) ),
inference(simp,[status(thm)],[47591]) ).
thf(311,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( a @ ( b @ mult ) ) )
| ( ( c @ ( a @ ( B @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,15]) ).
thf(337,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= a )
| ( A != b )
| ( ( c @ ( a @ ( B @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[311]) ).
thf(376,plain,
! [A: $i] :
( ( ( A @ ( b @ ld ) )
!= a )
| ( ( c @ ( a @ ( A @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[337]) ).
thf(38196,plain,
! [A: $i] :
( ( ( b @ ( A @ i @ mult ) @ i )
!= a )
| ( ( c @ ( a @ ( A @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(rewrite,[status(thm)],[376,2318]) ).
thf(553,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ mult ) @ ( A @ ld ) )
!= ( unit @ ( C @ i @ ld ) ) )
| ( B = C ) ),
inference(paramod_ordered,[status(thm)],[19,531]) ).
thf(561,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ mult ) )
!= unit )
| ( A
!= ( C @ i ) )
| ( B = C ) ),
inference(simp,[status(thm)],[553]) ).
thf(563,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) )
!= unit )
| ( A = B ) ),
inference(simp,[status(thm)],[561]) ).
thf(12829,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( a @ i ) )
| ( ( b @ i )
!= unit )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[11079,11917]) ).
thf(12863,plain,
( ( ( unit @ ( unit @ rd ) )
!= a )
| ( ( b @ i )
!= unit ) ),
inference(simp,[status(thm)],[12829]) ).
thf(14877,plain,
( ( ( unit @ i )
!= a )
| ( ( b @ i )
!= unit ) ),
inference(rewrite,[status(thm)],[12863,802]) ).
thf(95446,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ ( b @ rd ) @ ( unit @ rd ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[20919,86342]) ).
thf(95447,plain,
( ( unit @ i @ i @ ( b @ rd ) @ ( unit @ rd ) )
!= a ),
inference(pattern_uni,[status(thm)],[95446:[bind(A,$thf( unit @ i @ i ))]]) ).
thf(97891,plain,
( ( unit @ i @ i @ ( b @ rd ) @ i )
!= a ),
inference(rewrite,[status(thm)],[95447,802]) ).
thf(851,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ mult ) @ ( A @ ld ) )
!= ( C @ ( D @ ( C @ rd ) @ ld ) ) )
| ( B = D ) ),
inference(paramod_ordered,[status(thm)],[19,712]) ).
thf(864,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ mult ) )
!= C )
| ( A
!= ( D @ ( C @ rd ) ) )
| ( B = D ) ),
inference(simp,[status(thm)],[851]) ).
thf(868,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( C @ ( B @ rd ) @ mult ) )
!= B )
| ( A = C ) ),
inference(simp,[status(thm)],[864]) ).
thf(26632,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
!= ( a @ ( unit @ i @ rd ) ) )
| ( A != b ) ),
inference(paramod_ordered,[status(thm)],[1825,26620]) ).
thf(26669,plain,
! [A: $i] :
( ( ( b @ ( A @ i @ mult ) @ i )
!= a )
| ( A
!= ( unit @ i ) ) ),
inference(simp,[status(thm)],[26632]) ).
thf(26685,plain,
( ( b @ ( unit @ i @ i @ mult ) @ i )
!= a ),
inference(simp,[status(thm)],[26669]) ).
thf(26690,plain,
( ( b @ ( unit @ mult ) @ i )
!= a ),
inference(rewrite,[status(thm)],[26685,20045]) ).
thf(651,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( ( A @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,15]) ).
thf(670,plain,
! [B: $i,A: $i] :
( ( B != c )
| ( ( B @ ( A @ rd ) )
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( A @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[651]) ).
thf(722,plain,
! [A: $i] :
( ( ( c @ ( A @ rd ) )
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( A @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[670]) ).
thf(12890,plain,
( ( ( unit @ i )
!= ( a @ i ) )
| ( b != a )
| ( unit != unit ) ),
inference(paramod_ordered,[status(thm)],[43,12856]) ).
thf(12891,plain,
( ( ( unit @ i )
!= ( a @ i ) )
| ( b != a ) ),
inference(simp,[status(thm)],[12890]) ).
thf(12903,plain,
( ( unit != a )
| ( b != a ) ),
inference(simp,[status(thm)],[12891]) ).
thf(27869,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( a @ ( unit @ rd ) ) )
| ( A
!= ( b @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1829,27859]) ).
thf(27876,plain,
( ( b @ i @ i @ i @ ( unit @ rd ) )
!= ( a @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[27869]) ).
thf(29610,plain,
( ( b @ i @ i @ i @ i )
!= ( a @ i ) ),
inference(rewrite,[status(thm)],[27876,802]) ).
thf(131,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ i )
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( unit != a ) ),
inference(simp,[status(thm)],[71]) ).
thf(145,plain,
( ( ( b @ ( a @ mult ) )
!= ( a @ i ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( unit != a ) ),
inference(simp,[status(thm)],[131]) ).
thf(25212,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
!= ( b @ ( a @ i @ rd ) ) )
| ( A
!= ( unit @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1825,25201]) ).
thf(25250,plain,
! [A: $i] :
( ( ( unit @ i @ i @ ( A @ i @ mult ) @ i )
!= b )
| ( A
!= ( a @ i ) ) ),
inference(simp,[status(thm)],[25212]) ).
thf(25271,plain,
( ( unit @ i @ i @ ( a @ i @ i @ mult ) @ i )
!= b ),
inference(simp,[status(thm)],[25250]) ).
thf(26046,plain,
( ( unit @ ( a @ mult ) @ i )
!= b ),
inference(rewrite,[status(thm)],[25271,571,20045]) ).
thf(3966,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( C @ ( C @ rd ) ) )
| ( A != a )
| ( unit != b ) ),
inference(paramod_ordered,[status(thm)],[23,3652]) ).
thf(3979,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ ( a @ mult ) )
!= B )
| ( unit != b ) ),
inference(simp,[status(thm)],[3966]) ).
thf(3988,plain,
! [A: $i] :
( ( ( A @ ( a @ mult ) )
!= A )
| ( unit != b ) ),
inference(simp,[status(thm)],[3979]) ).
thf(431,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( unit @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,15]) ).
thf(472,plain,
! [A: $i] :
( ( ( A @ i )
!= a )
| ( A
!= ( a @ ( b @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( unit @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[431]) ).
thf(497,plain,
( ( ( a @ ( b @ mult ) @ i )
!= a )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( unit @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[472]) ).
thf(62427,plain,
( ( ( a @ ( b @ mult ) @ i )
!= a )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[497,27]) ).
thf(95417,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ ( b @ rd ) @ ( unit @ rd ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[21498,86342]) ).
thf(95418,plain,
( ( unit @ i @ i @ i @ ( b @ rd ) @ ( unit @ rd ) )
!= a ),
inference(pattern_uni,[status(thm)],[95417:[bind(A,$thf( unit @ i @ i @ i ))]]) ).
thf(98071,plain,
( ( unit @ i @ i @ i @ ( b @ rd ) @ i )
!= a ),
inference(rewrite,[status(thm)],[95418,802]) ).
thf(71029,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( a @ i @ ( C @ mult ) ) )
| ( A
!= ( b @ ( C @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,47919]) ).
thf(71030,plain,
! [A: $i] :
( ( b @ ( a @ i @ ( A @ rd ) @ mult ) )
!= A ),
inference(pattern_uni,[status(thm)],[71029:[bind(A,$thf( D )),bind(B,$thf( a @ i )),bind(C,$thf( a @ i @ ( D @ rd ) ))]]) ).
thf(71205,plain,
! [A: $i] :
( ( b @ ( a @ i @ ( A @ rd ) @ mult ) )
!= A ),
inference(simp,[status(thm)],[71030]) ).
thf(75230,plain,
! [A: $i] :
( ( ( b @ ( a @ i @ ( A @ rd ) @ mult ) )
!= ( unit @ ( unit @ mult ) ) )
| ( unit != A ) ),
inference(paramod_ordered,[status(thm)],[48733,71205]) ).
thf(75263,plain,
( ( b @ ( a @ i @ ( unit @ rd ) @ mult ) )
!= ( unit @ ( unit @ mult ) ) ),
inference(simp,[status(thm)],[75230]) ).
thf(75871,plain,
( ( b @ ( a @ i @ i @ mult ) )
!= unit ),
inference(rewrite,[status(thm)],[75263,802,48733]) ).
thf(41887,plain,
( ( unit @ ( unit @ rd ) )
!= ( b @ ( unit @ i @ rd ) @ ( a @ rd ) ) ),
inference(simp,[status(thm)],[41878]) ).
thf(44248,plain,
( ( b @ ( unit @ rd ) @ ( a @ rd ) )
!= unit ),
inference(rewrite,[status(thm)],[41887,43,21387]) ).
thf(640,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( C @ ( C @ ( B @ rd ) @ mult ) ) )
| ( unit = B ) ),
inference(paramod_ordered,[status(thm)],[35,21]) ).
thf(689,plain,
! [C: $i,B: $i,A: $i] :
( ( A != C )
| ( ( A @ i )
!= ( C @ ( B @ rd ) ) )
| ( unit = B ) ),
inference(simp,[status(thm)],[640]) ).
thf(739,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ rd ) )
!= ( B @ i ) )
| ( unit = A ) ),
inference(simp,[status(thm)],[689]) ).
thf(921,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( D @ ( D @ ( C @ rd ) @ mult ) ) )
| ( ( B @ i )
= C ) ),
inference(paramod_ordered,[status(thm)],[29,21]) ).
thf(961,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= D )
| ( A
!= ( D @ ( C @ rd ) ) )
| ( ( B @ i )
= C ) ),
inference(simp,[status(thm)],[921]) ).
thf(1003,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ rd ) @ ( A @ mult ) @ i )
!= C )
| ( ( A @ i )
= B ) ),
inference(simp,[status(thm)],[961]) ).
thf(78,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( unit @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,15]) ).
thf(121,plain,
! [A: $i] :
( ( A != c )
| ( ( A @ i )
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( unit @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[78]) ).
thf(182,plain,
( ( ( a @ ( a @ ( b @ mult ) @ mult ) )
!= ( c @ i ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( unit @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[121]) ).
thf(21193,plain,
( ( ( a @ ( a @ ( b @ mult ) @ mult ) )
!= ( c @ i ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= a ) ),
inference(rewrite,[status(thm)],[182,25]) ).
thf(46,plain,
! [B: $i,A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( B @ ( unit @ mult ) ) )
| ( unit = B ) ),
inference(paramod_ordered,[status(thm)],[35,27]) ).
thf(48,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ i )
!= unit )
| ( unit = B ) ),
inference(simp,[status(thm)],[46]) ).
thf(50,plain,
! [A: $i] :
( ( ( A @ i )
!= unit )
| ( unit = A ) ),
inference(simp,[status(thm)],[48]) ).
thf(77513,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) )
!= ( unit @ ( b @ rd ) ) )
| ( ( A @ i @ ( a @ mult ) )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[802,77505]) ).
thf(77568,plain,
! [A: $i] :
( ( A != unit )
| ( unit != b )
| ( ( A @ i @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[77513]) ).
thf(77586,plain,
( ( unit != b )
| ( ( unit @ i @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[77568]) ).
thf(78252,plain,
( ( unit != b )
| ( ( unit @ ( a @ mult ) )
!= unit ) ),
inference(rewrite,[status(thm)],[77586,43]) ).
thf(18651,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( C @ ( C @ rd ) ) )
| ( A != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[23,12902]) ).
thf(18655,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ ( a @ mult ) )
!= B )
| ( b != a ) ),
inference(simp,[status(thm)],[18651]) ).
thf(18666,plain,
! [A: $i] :
( ( ( A @ ( a @ mult ) )
!= A )
| ( b != a ) ),
inference(simp,[status(thm)],[18655]) ).
thf(352,plain,
! [A: $i] :
( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) @ ( A @ ld ) @ ( A @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ),
inference(simp,[status(thm)],[309]) ).
thf(30104,plain,
! [A: $i] :
( ( A @ ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) @ i @ mult ) @ i @ ( A @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ),
inference(rewrite,[status(thm)],[352,2318]) ).
thf(537,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ mult ) @ ( A @ ld ) )
!= ( C @ ( C @ ld ) ) )
| ( B = unit ) ),
inference(paramod_ordered,[status(thm)],[19,525]) ).
thf(542,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ mult ) )
!= C )
| ( A != C )
| ( B = unit ) ),
inference(simp,[status(thm)],[537]) ).
thf(544,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) )
!= B )
| ( A = unit ) ),
inference(simp,[status(thm)],[542]) ).
thf(9,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ mult ) @ ( A @ mult ) )
= ( C @ ( A @ mult ) @ ( A @ ( B @ ( A @ mult ) @ rd ) @ mult ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c08) ).
thf(30,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ mult ) @ ( A @ mult ) )
= ( C @ ( A @ mult ) @ ( A @ ( B @ ( A @ mult ) @ rd ) @ mult ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(31,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ mult ) @ ( A @ ( B @ ( A @ mult ) @ rd ) @ mult ) )
= ( C @ ( B @ mult ) @ ( A @ mult ) ) ),
inference(lifteq,[status(thm)],[30]) ).
thf(38067,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( C @ ( C @ i @ mult ) ) )
| ( A
!= ( b @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21,14259]) ).
thf(38112,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ ( b @ ( a @ mult ) @ rd ) )
!= ( B @ i ) ) ),
inference(simp,[status(thm)],[38067]) ).
thf(38126,plain,
! [A: $i] :
( ( A @ ( b @ ( a @ mult ) @ rd ) )
!= ( A @ i ) ),
inference(simp,[status(thm)],[38112]) ).
thf(675,plain,
! [A: $i] :
( ( A
!= ( c @ ( a @ mult ) ) )
| ( ( A @ ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) @ rd ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[646]) ).
thf(727,plain,
( ( c @ ( a @ mult ) @ ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) @ rd ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) ),
inference(simp,[status(thm)],[675]) ).
thf(67,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( a @ ( b @ mult ) ) )
| ( ( c @ ( a @ ( A @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,15]) ).
thf(110,plain,
! [A: $i] :
( ( A != a )
| ( unit != b )
| ( ( c @ ( a @ ( A @ mult ) @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(175,plain,
( ( unit != b )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[110]) ).
thf(48430,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( unit @ ( A @ ( unit @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[23685,48409]) ).
thf(48431,plain,
( ( unit @ ( unit @ i @ i @ i @ i @ i @ i @ ( unit @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48430:[bind(A,$thf( unit @ i @ i @ i @ i @ i @ i ))]]) ).
thf(60568,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ ( unit @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48431,713]) ).
thf(13111,plain,
( ( ( unit @ i @ ( b @ mult ) @ i )
!= ( unit @ i ) )
| ( unit != a ) ),
inference(paramod_ordered,[status(thm)],[43,13082]) ).
thf(13129,plain,
( ( ( unit @ i @ ( b @ mult ) )
!= unit )
| ( unit != a ) ),
inference(simp,[status(thm)],[13111]) ).
thf(15841,plain,
( ( ( unit @ ( b @ mult ) )
!= unit )
| ( unit != a ) ),
inference(rewrite,[status(thm)],[13129,43]) ).
thf(312,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) )
| ( B
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[17,15]) ).
thf(328,plain,
! [A: $i] :
( ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) @ ( A @ ld ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( A != a ) ),
inference(simp,[status(thm)],[312]) ).
thf(370,plain,
( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) @ ( a @ ld ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) ),
inference(simp,[status(thm)],[328]) ).
thf(35201,plain,
( ( a @ ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) @ i @ mult ) @ i )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) ),
inference(rewrite,[status(thm)],[370,2318]) ).
thf(913,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( C @ i @ ( C @ mult ) ) )
| ( ( B @ i )
= unit ) ),
inference(paramod_ordered,[status(thm)],[29,37]) ).
thf(927,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= ( C @ i ) )
| ( A != C )
| ( ( B @ i )
= unit ) ),
inference(simp,[status(thm)],[913]) ).
thf(976,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ mult ) @ i )
!= ( B @ i ) )
| ( ( A @ i )
= unit ) ),
inference(simp,[status(thm)],[927]) ).
thf(430,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[37,15]) ).
thf(469,plain,
! [A: $i] :
( ( ( A @ i )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( A != a )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[430]) ).
thf(495,plain,
( ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( a @ i ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[469]) ).
thf(38068,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( A @ ( unit @ mult ) )
!= ( b @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[21498,14259]) ).
thf(38069,plain,
( ( unit @ i @ i @ i @ ( unit @ mult ) )
!= ( b @ ( a @ mult ) ) ),
inference(pattern_uni,[status(thm)],[38068:[bind(A,$thf( unit @ i @ i @ i ))]]) ).
thf(38751,plain,
( ( b @ ( a @ mult ) )
!= ( unit @ i @ i @ i ) ),
inference(rewrite,[status(thm)],[38069,27]) ).
thf(327,plain,
! [A: $i] :
( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) @ ( A @ ld ) @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ),
inference(simp,[status(thm)],[312]) ).
thf(27903,plain,
! [A: $i] :
( ( A @ ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) @ i @ mult ) @ i @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ),
inference(rewrite,[status(thm)],[327,2318]) ).
thf(48535,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( unit @ ( A @ ( unit @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[34257,48409]) ).
thf(48536,plain,
( ( unit @ ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ ( unit @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48535:[bind(A,$thf( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i ))]]) ).
thf(82107,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ i @ i @ i @ ( unit @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48536,713]) ).
thf(329,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( B != a ) ),
inference(simp,[status(thm)],[307]) ).
thf(371,plain,
! [A: $i] :
( ( ( a @ ( A @ ld ) @ ( A @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[329]) ).
thf(35537,plain,
! [A: $i] :
( ( ( A @ ( a @ i @ mult ) @ i @ ( A @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[371,2318]) ).
thf(68,plain,
! [A: $i] :
( ( ( A @ ( unit @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) )
| ( A
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[27,15]) ).
thf(139,plain,
( ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) )
| ( unit != a ) ),
inference(simp,[status(thm)],[68]) ).
thf(48104,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( C @ ( C @ rd ) ) )
| ( A
!= ( b @ i @ ( a @ rd ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,42071]) ).
thf(48159,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ ( b @ i @ ( a @ rd ) @ mult ) )
!= B ) ),
inference(simp,[status(thm)],[48104]) ).
thf(48224,plain,
! [A: $i] :
( ( A @ ( b @ i @ ( a @ rd ) @ mult ) )
!= A ),
inference(simp,[status(thm)],[48159]) ).
thf(13790,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( b @ ( a @ mult ) @ i ) )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[11079,13773]) ).
thf(13810,plain,
( ( unit @ ( unit @ rd ) )
!= ( b @ ( a @ mult ) ) ),
inference(simp,[status(thm)],[13790]) ).
thf(13998,plain,
( ( b @ ( a @ mult ) )
!= ( unit @ i ) ),
inference(rewrite,[status(thm)],[13810,802]) ).
thf(25224,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( b @ ( a @ i @ rd ) ) )
| ( A
!= ( unit @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[23,25201]) ).
thf(25254,plain,
! [A: $i] :
( ( A != b )
| ( ( A @ ( unit @ i @ i @ mult ) )
!= ( a @ i ) ) ),
inference(simp,[status(thm)],[25224]) ).
thf(25273,plain,
( ( b @ ( unit @ i @ i @ mult ) )
!= ( a @ i ) ),
inference(simp,[status(thm)],[25254]) ).
thf(25282,plain,
( ( b @ ( unit @ mult ) )
!= ( a @ i ) ),
inference(rewrite,[status(thm)],[25273,20045]) ).
thf(47194,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( C @ ( C @ rd ) ) )
| ( A
!= ( a @ i @ ( b @ rd ) ) ) ),
inference(paramod_ordered,[status(thm)],[23,32892]) ).
thf(47239,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( A @ ( a @ i @ ( b @ rd ) @ mult ) )
!= B ) ),
inference(simp,[status(thm)],[47194]) ).
thf(47297,plain,
! [A: $i] :
( ( A @ ( a @ i @ ( b @ rd ) @ mult ) )
!= A ),
inference(simp,[status(thm)],[47239]) ).
thf(76609,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ i @ mult ) @ i @ ( B @ rd ) )
!= ( unit @ ( b @ rd ) ) )
| ( A
!= ( a @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1825,76604]) ).
thf(76635,plain,
! [A: $i] :
( ( ( a @ i @ ( A @ i @ mult ) @ i )
!= unit )
| ( A != b ) ),
inference(simp,[status(thm)],[76609]) ).
thf(76649,plain,
( ( a @ i @ ( b @ i @ mult ) @ i )
!= unit ),
inference(simp,[status(thm)],[76635]) ).
thf(19326,plain,
! [A: $i] :
( ( ( A @ i @ ( unit @ rd ) )
!= ( b @ ( unit @ rd ) ) )
| ( A
!= ( a @ i @ i ) ) ),
inference(paramod_ordered,[status(thm)],[1829,19318]) ).
thf(19327,plain,
( ( a @ i @ i @ i @ ( unit @ rd ) )
!= ( b @ ( unit @ rd ) ) ),
inference(simp,[status(thm)],[19326]) ).
thf(19721,plain,
( ( a @ i @ i @ i @ i )
!= ( b @ i ) ),
inference(rewrite,[status(thm)],[19327,802]) ).
thf(48459,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( unit @ ( A @ ( unit @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[21498,48409]) ).
thf(48460,plain,
( ( unit @ ( unit @ i @ i @ i @ ( unit @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48459:[bind(A,$thf( unit @ i @ i @ i ))]]) ).
thf(53982,plain,
( ( unit @ i @ i @ i @ ( unit @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48460,713]) ).
thf(664,plain,
! [B: $i,A: $i] :
( ( B != b )
| ( ( B @ ( A @ rd ) )
!= a )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( A @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[645]) ).
thf(716,plain,
! [A: $i] :
( ( ( b @ ( A @ rd ) )
!= a )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( A @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[664]) ).
thf(57,plain,
! [A: $i] :
( ( ( unit @ ( A @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) )
| ( A
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,15]) ).
thf(119,plain,
( ( ( c @ ( a @ mult ) )
!= unit )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[57]) ).
thf(955,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= b )
| ( A != a )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( B @ i @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[902]) ).
thf(999,plain,
! [A: $i] :
( ( ( a @ ( A @ mult ) @ i )
!= b )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( A @ i @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[955]) ).
thf(323,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= b )
| ( A != a )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( B @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[308]) ).
thf(366,plain,
! [A: $i] :
( ( ( A @ ( a @ ld ) )
!= b )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( A @ mult ) )
!= a ) ),
inference(simp,[status(thm)],[323]) ).
thf(33629,plain,
! [A: $i] :
( ( ( a @ ( A @ i @ mult ) @ i )
!= b )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( a @ ( A @ mult ) )
!= a ) ),
inference(rewrite,[status(thm)],[366,2318]) ).
thf(86872,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ rd ) @ ( A @ mult ) )
!= ( b @ ( a @ i @ ( B @ rd ) @ mult ) ) )
| ( unit != B ) ),
inference(paramod_ordered,[status(thm)],[86370,71205]) ).
thf(87087,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) )
!= b )
| ( A
!= ( a @ i @ ( unit @ rd ) ) ) ),
inference(simp,[status(thm)],[86872]) ).
thf(88056,plain,
( ( a @ i @ ( unit @ rd ) @ ( unit @ rd ) )
!= b ),
inference(simp,[status(thm)],[87087]) ).
thf(92979,plain,
( ( a @ i @ ( unit @ rd ) @ i )
!= b ),
inference(rewrite,[status(thm)],[88056,802]) ).
thf(76,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[35,15]) ).
thf(102,plain,
! [A: $i] :
( ( A
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( ( A @ i )
!= a )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[76]) ).
thf(168,plain,
( ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ i )
!= a )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[102]) ).
thf(6038,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ rd ) @ ld ) )
!= ( C @ ( C @ ld ) ) )
| ( B != b )
| ( unit != a ) ),
inference(paramod_ordered,[status(thm)],[712,5428]) ).
thf(6045,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( b @ ( A @ rd ) )
!= B )
| ( unit != a ) ),
inference(simp,[status(thm)],[6038]) ).
thf(6050,plain,
! [A: $i] :
( ( ( b @ ( A @ rd ) )
!= A )
| ( unit != a ) ),
inference(simp,[status(thm)],[6045]) ).
thf(684,plain,
! [A: $i] :
( ( A @ ( A @ ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) @ rd ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ),
inference(simp,[status(thm)],[649]) ).
thf(735,plain,
! [A: $i] :
( ( A @ ( A @ ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) @ rd ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ),
inference(simp,[status(thm)],[684]) ).
thf(47823,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( a @ i @ ( C @ mult ) ) )
| ( ( b @ ( A @ rd ) )
!= C ) ),
inference(paramod_ordered,[status(thm)],[21,41953]) ).
thf(47824,plain,
! [A: $i] :
( ( a @ i @ ( A @ rd ) )
!= ( b @ ( A @ rd ) ) ),
inference(pattern_uni,[status(thm)],[47823:[bind(A,$thf( D )),bind(B,$thf( a @ i )),bind(C,$thf( a @ i @ ( D @ rd ) ))]]) ).
thf(47921,plain,
! [A: $i] :
( ( a @ i @ ( A @ rd ) )
!= ( b @ ( A @ rd ) ) ),
inference(simp,[status(thm)],[47824]) ).
thf(77,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( unit @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[35,15]) ).
thf(93,plain,
! [A: $i] :
( ( A != a )
| ( ( A @ i )
!= ( a @ ( b @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( unit @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[77]) ).
thf(161,plain,
( ( ( a @ ( b @ mult ) )
!= ( a @ i ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( unit @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[93]) ).
thf(16041,plain,
( ( ( a @ ( b @ mult ) )
!= ( a @ i ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[161,27]) ).
thf(330,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= a )
| ( A
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( B @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[307]) ).
thf(372,plain,
! [A: $i] :
( ( ( A @ ( b @ ( a @ mult ) @ ld ) )
!= a )
| ( ( c @ ( a @ mult ) @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[330]) ).
thf(36844,plain,
! [A: $i] :
( ( ( b @ ( a @ mult ) @ ( A @ i @ mult ) @ i )
!= a )
| ( ( c @ ( a @ mult ) @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[372,2318]) ).
thf(84926,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( C @ ( a @ rd ) @ ( b @ mult ) ) )
| ( ( A @ i )
!= C ) ),
inference(paramod_ordered,[status(thm)],[21,76114]) ).
thf(85021,plain,
! [B: $i,A: $i] :
( ( B
!= ( A @ i @ ( a @ rd ) ) )
| ( ( B @ ( A @ rd ) )
!= b ) ),
inference(simp,[status(thm)],[84926]) ).
thf(85076,plain,
! [A: $i] :
( ( A @ i @ ( a @ rd ) @ ( A @ rd ) )
!= b ),
inference(simp,[status(thm)],[85021]) ).
thf(683,plain,
! [A: $i] :
( ( A != b )
| ( ( A @ ( unit @ rd ) )
!= a )
| ( b != a ) ),
inference(simp,[status(thm)],[641]) ).
thf(734,plain,
( ( ( b @ ( unit @ rd ) )
!= a )
| ( b != a ) ),
inference(simp,[status(thm)],[683]) ).
thf(793,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( b @ ( unit @ rd ) ) )
| ( A != a )
| ( b != a ) ),
inference(paramod_ordered,[status(thm)],[23,734]) ).
thf(798,plain,
! [A: $i] :
( ( ( A @ ( A @ ( a @ mult ) @ rd ) )
!= ( b @ ( unit @ rd ) ) )
| ( b != a ) ),
inference(simp,[status(thm)],[793]) ).
thf(805,plain,
! [A: $i] :
( ( ( A @ ( A @ ( a @ mult ) @ rd ) )
!= ( b @ ( unit @ rd ) ) )
| ( b != a ) ),
inference(simp,[status(thm)],[798]) ).
thf(99978,plain,
! [A: $i] :
( ( ( A @ ( A @ ( a @ mult ) @ rd ) )
!= ( b @ i ) )
| ( b != a ) ),
inference(rewrite,[status(thm)],[805,802]) ).
thf(319,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) @ ( A @ mult ) )
!= ( unit @ ( C @ mult ) ) )
| ( B = C ) ),
inference(paramod_ordered,[status(thm)],[17,25]) ).
thf(363,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= unit )
| ( A != C )
| ( B = C ) ),
inference(simp,[status(thm)],[319]) ).
thf(398,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ld ) )
!= unit )
| ( A = B ) ),
inference(simp,[status(thm)],[363]) ).
thf(45670,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ i @ mult ) @ i )
!= unit )
| ( A = B ) ),
inference(rewrite,[status(thm)],[398,2318]) ).
thf(925,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i @ i )
!= ( B @ ( C @ mult ) @ i ) )
| ( ( A @ ( B @ mult ) )
= ( C @ i ) ) ),
inference(paramod_ordered,[status(thm)],[571,29]) ).
thf(960,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ i )
!= ( B @ ( C @ mult ) ) )
| ( ( A @ ( B @ mult ) )
= ( C @ i ) ) ),
inference(simp,[status(thm)],[925]) ).
thf(829,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( unit @ rd ) )
!= ( C @ ( C @ ( B @ mult ) @ rd ) ) )
| ( ( A @ i )
= B ) ),
inference(paramod_ordered,[status(thm)],[802,23]) ).
thf(837,plain,
! [C: $i,B: $i,A: $i] :
( ( A != C )
| ( ( C @ ( B @ mult ) )
!= unit )
| ( ( A @ i )
= B ) ),
inference(simp,[status(thm)],[829]) ).
thf(839,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ mult ) )
!= unit )
| ( ( B @ i )
= A ) ),
inference(simp,[status(thm)],[837]) ).
thf(656,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ rd ) @ mult ) )
!= ( C @ i @ ( C @ mult ) ) )
| ( A = unit ) ),
inference(paramod_ordered,[status(thm)],[21,37]) ).
thf(690,plain,
! [C: $i,B: $i,A: $i] :
( ( B
!= ( C @ i ) )
| ( ( B @ ( A @ rd ) )
!= C )
| ( A = unit ) ),
inference(simp,[status(thm)],[656]) ).
thf(740,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ rd ) @ i )
!= B )
| ( A = unit ) ),
inference(simp,[status(thm)],[690]) ).
thf(907,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( c @ ( B @ i @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,15]) ).
thf(941,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= a )
| ( A
!= ( a @ ( b @ mult ) ) )
| ( ( c @ ( B @ i @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[907]) ).
thf(987,plain,
! [A: $i] :
( ( ( a @ ( b @ mult ) @ ( A @ mult ) @ i )
!= a )
| ( ( c @ ( A @ i @ mult ) @ ( a @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) ) ),
inference(simp,[status(thm)],[941]) ).
thf(86183,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ mult ) @ rd ) )
!= ( C @ ( C @ rd ) @ ( b @ rd ) ) )
| ( A
!= ( a @ i ) ) ),
inference(paramod_ordered,[status(thm)],[23,76417]) ).
thf(86201,plain,
! [B: $i,A: $i] :
( ( A
!= ( B @ ( B @ rd ) ) )
| ( ( A @ ( a @ i @ mult ) )
!= b ) ),
inference(simp,[status(thm)],[86183]) ).
thf(86235,plain,
! [A: $i] :
( ( A @ ( A @ rd ) @ ( a @ i @ mult ) )
!= b ),
inference(simp,[status(thm)],[86201]) ).
thf(322,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ld ) )
!= b )
| ( A != a )
| ( ( c @ ( a @ mult ) @ ( a @ ( B @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[308]) ).
thf(365,plain,
! [A: $i] :
( ( ( A @ ( a @ ld ) )
!= b )
| ( ( c @ ( a @ mult ) @ ( a @ ( A @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[322]) ).
thf(33037,plain,
! [A: $i] :
( ( ( a @ ( A @ i @ mult ) @ i )
!= b )
| ( ( c @ ( a @ mult ) @ ( a @ ( A @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[365,2318]) ).
thf(892,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i @ ( A @ mult ) )
!= ( C @ ( C @ i @ mult ) ) )
| ( ( B @ i )
= unit ) ),
inference(paramod_ordered,[status(thm)],[29,35]) ).
thf(947,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= C )
| ( A
!= ( C @ i ) )
| ( ( B @ i )
= unit ) ),
inference(simp,[status(thm)],[892]) ).
thf(992,plain,
! [B: $i,A: $i] :
( ( ( B @ i @ ( A @ mult ) @ i )
!= B )
| ( ( A @ i )
= unit ) ),
inference(simp,[status(thm)],[947]) ).
thf(73,plain,
! [A: $i] :
( ( ( A @ ( A @ i @ mult ) )
!= ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) )
!= unit ) ),
inference(paramod_ordered,[status(thm)],[35,15]) ).
thf(95,plain,
! [A: $i] :
( ( A
!= ( c @ ( a @ mult ) ) )
| ( ( A @ i )
!= ( a @ ( b @ ( a @ mult ) @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[73]) ).
thf(163,plain,
( ( ( a @ ( b @ ( a @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) @ i ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) )
!= unit ) ),
inference(simp,[status(thm)],[95]) ).
thf(934,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ mult ) @ i )
!= a )
| ( A
!= ( b @ ( a @ mult ) ) )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( B @ i )
!= a ) ),
inference(simp,[status(thm)],[901]) ).
thf(982,plain,
! [A: $i] :
( ( ( b @ ( a @ mult ) @ ( A @ mult ) @ i )
!= a )
| ( ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( A @ i )
!= a ) ),
inference(simp,[status(thm)],[934]) ).
thf(48554,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( unit @ ( A @ ( unit @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[24324,48409]) ).
thf(48555,plain,
( ( unit @ ( unit @ i @ i @ i @ i @ i @ i @ i @ ( unit @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48554:[bind(A,$thf( unit @ i @ i @ i @ i @ i @ i @ i ))]]) ).
thf(62935,plain,
( ( unit @ i @ i @ i @ i @ i @ i @ i @ ( unit @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48555,713]) ).
thf(86391,plain,
! [B: $i,A: $i] :
( ( ( A @ ( unit @ rd ) @ ( A @ mult ) )
!= ( a @ i @ ( B @ mult ) ) )
| ( ( b @ ( unit @ rd ) )
!= B ) ),
inference(paramod_ordered,[status(thm)],[86370,41953]) ).
thf(87080,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) )
!= ( a @ i ) )
| ( A
!= ( b @ ( unit @ rd ) ) ) ),
inference(simp,[status(thm)],[86391]) ).
thf(88052,plain,
( ( b @ ( unit @ rd ) @ ( unit @ rd ) )
!= ( a @ i ) ),
inference(simp,[status(thm)],[87080]) ).
thf(92851,plain,
( ( b @ ( unit @ rd ) @ i )
!= ( a @ i ) ),
inference(rewrite,[status(thm)],[88052,802]) ).
thf(48479,plain,
! [A: $i] :
( ( ( unit @ i @ i @ i @ i @ i @ i )
!= ( A @ i ) )
| ( ( unit @ ( A @ ( unit @ mult ) @ rd ) )
= unit ) ),
inference(paramod_ordered,[status(thm)],[22781,48409]) ).
thf(48480,plain,
( ( unit @ ( unit @ i @ i @ i @ i @ i @ ( unit @ mult ) @ rd ) )
= unit ),
inference(pattern_uni,[status(thm)],[48479:[bind(A,$thf( unit @ i @ i @ i @ i @ i ))]]) ).
thf(58451,plain,
( ( unit @ i @ i @ i @ i @ i @ ( unit @ mult ) )
= unit ),
inference(rewrite,[status(thm)],[48480,713]) ).
thf(850,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ rd ) @ ld ) )
!= ( D @ ( C @ mult ) @ ( C @ ld ) ) )
| ( B = D ) ),
inference(paramod_ordered,[status(thm)],[712,19]) ).
thf(867,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A
!= ( D @ ( C @ mult ) ) )
| ( ( B @ ( A @ rd ) )
!= C )
| ( B = D ) ),
inference(simp,[status(thm)],[850]) ).
thf(871,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ ( A @ rd ) @ mult ) )
!= A )
| ( B = C ) ),
inference(simp,[status(thm)],[867]) ).
thf(428,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( c @ ( a @ mult ) ) )
| ( ( unit @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,15]) ).
thf(443,plain,
! [A: $i] :
( ( ( A @ i )
!= c )
| ( A != a )
| ( ( unit @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[428]) ).
thf(503,plain,
( ( ( a @ i )
!= c )
| ( ( unit @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[443]) ).
thf(67549,plain,
( ( ( a @ i )
!= c )
| ( ( a @ ( b @ ( a @ mult ) @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) @ ( a @ mult ) ) ) ),
inference(rewrite,[status(thm)],[503,25]) ).
thf(95462,plain,
! [A: $i] :
( ( ( unit @ i @ i )
!= ( A @ i ) )
| ( ( A @ ( b @ rd ) @ ( unit @ rd ) )
!= a ) ),
inference(paramod_ordered,[status(thm)],[20045,86342]) ).
thf(95463,plain,
( ( unit @ i @ ( b @ rd ) @ ( unit @ rd ) )
!= a ),
inference(pattern_uni,[status(thm)],[95462:[bind(A,$thf( unit @ i ))]]) ).
thf(97756,plain,
( ( unit @ i @ ( b @ rd ) @ i )
!= a ),
inference(rewrite,[status(thm)],[95463,802]) ).
thf(14753,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( a @ i ) )
| ( ( b @ i )
!= ( a @ i ) )
| ( A != unit ) ),
inference(paramod_ordered,[status(thm)],[11079,12855]) ).
thf(14777,plain,
( ( ( unit @ ( unit @ rd ) )
!= a )
| ( ( b @ i )
!= ( a @ i ) ) ),
inference(simp,[status(thm)],[14753]) ).
thf(19427,plain,
( ( ( unit @ i )
!= a )
| ( ( b @ i )
!= ( a @ i ) ) ),
inference(rewrite,[status(thm)],[14777,802]) ).
thf(5557,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ rd ) @ ld ) )
!= ( C @ ( C @ ld ) ) )
| ( B != a )
| ( unit != b ) ),
inference(paramod_ordered,[status(thm)],[712,5412]) ).
thf(5564,plain,
! [B: $i,A: $i] :
( ( A != B )
| ( ( a @ ( A @ rd ) )
!= B )
| ( unit != b ) ),
inference(simp,[status(thm)],[5557]) ).
thf(5569,plain,
! [A: $i] :
( ( ( a @ ( A @ rd ) )
!= A )
| ( unit != b ) ),
inference(simp,[status(thm)],[5564]) ).
thf(11130,plain,
! [A: $i] :
( ( ( A @ ( unit @ rd ) @ i )
!= ( b @ i ) )
| ( A != unit )
| ( unit != a ) ),
inference(paramod_ordered,[status(thm)],[11079,3700]) ).
thf(11182,plain,
( ( ( unit @ ( unit @ rd ) )
!= b )
| ( unit != a ) ),
inference(simp,[status(thm)],[11130]) ).
thf(11241,plain,
( ( ( unit @ i )
!= b )
| ( unit != a ) ),
inference(rewrite,[status(thm)],[11182,802]) ).
thf(432,plain,
! [A: $i] :
( ( ( A @ i @ ( A @ mult ) )
!= ( c @ ( a @ ( a @ ( b @ mult ) @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( unit @ ( a @ mult ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,15]) ).
thf(475,plain,
! [A: $i] :
( ( ( A @ i )
!= c )
| ( A
!= ( a @ ( a @ ( b @ mult ) @ mult ) ) )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( unit @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[432]) ).
thf(499,plain,
( ( ( a @ ( a @ ( b @ mult ) @ mult ) @ i )
!= c )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= ( unit @ ( a @ mult ) ) ) ),
inference(simp,[status(thm)],[475]) ).
thf(64859,plain,
( ( ( a @ ( a @ ( b @ mult ) @ mult ) @ i )
!= c )
| ( ( c @ ( a @ mult ) @ ( a @ ( b @ ( a @ mult ) @ mult ) @ mult ) )
!= a ) ),
inference(rewrite,[status(thm)],[499,25]) ).
thf(137582,plain,
$false,
inference(e,[status(thm)],[13024,72333,79445,34088,76417,43763,86361,16830,32802,32800,741,13811,32356,41953,977,170,40568,13675,3649,48409,11786,19242,2316,715,14805,11917,51851,85072,1001,782,39557,24,46983,23685,37,25,29914,19318,22320,76600,40440,43413,802,587,94269,105947,870,94068,81335,152,100683,29,44881,20,21820,85090,118341,46010,98555,75176,164,15398,42000,13647,77440,32256,821,76604,16448,47149,71781,877,46098,998,48403,12907,32023,981,766,47644,105032,65334,11079,68461,32840,46025,746,116864,11766,28,16386,40421,11217,630,18091,21,114252,729,11074,566,101627,37498,44103,41384,14259,46950,45928,27754,23604,156,21498,26620,19126,39667,40728,48031,989,742,74118,28713,57367,19879,78606,1207,94190,42071,46959,488,34189,6304,25423,25060,39005,1825,997,985,19181,47432,22781,984,129,12999,94420,108532,65310,95525,13,26325,41590,39618,40452,765,15344,24970,662,12902,32795,27859,81078,26402,81059,586,38809,22686,42257,98296,166,53931,46367,8728,26768,38146,180,3696,149,11920,32,34,33587,25201,41963,975,1884,22,743,67316,26604,18548,55661,545,27,2859,68904,11819,5567,107534,713,42215,77505,3700,44823,11792,85860,105491,13773,86,159,6048,45987,48049,736,81117,737,68892,15453,14042,990,996,45377,47919,86342,43498,494,53761,24193,30925,19357,726,91,12744,24968,45930,46451,47632,38196,563,90704,48733,14877,13737,41955,97891,6930,868,26690,35,722,2318,34257,12903,29610,145,86370,26591,11030,26046,3988,62427,98071,18,75871,44248,739,48230,25334,74356,1003,21193,50,25119,50298,78252,20919,76114,18666,16,30104,544,31,3652,38126,727,175,60568,12856,43,28857,24324,15841,571,3288,13082,7904,35201,976,495,38751,27903,82107,35537,47337,26,24962,139,48224,13998,23,71205,11780,25282,47297,76649,19721,53982,716,119,20045,3992,999,33629,92979,36,168,30,6050,735,47921,16041,36844,85076,99978,45670,960,22235,46948,68290,839,740,987,1829,12855,86235,33037,992,15,163,982,62935,92851,58451,871,71555,67549,22183,97756,19427,5569,11241,64859,32892,76588,13743]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP696-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.12/0.39 % Computer : n008.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Fri Sep 25 15:38:24 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.33/1.23 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.69/1.49 % [INFO] Parsing done (255ms).
% 1.89/1.51 % [INFO] Running in sequential loop mode.
% 2.45/2.02 % [INFO] eprover registered as external prover.
% 2.45/2.03 % [INFO] Scanning for conjecture ...
% 2.77/2.13 % [INFO] Found a conjecture (or negated_conjecture) and 11 axioms. Running axiom selection ...
% 2.92/2.16 % [INFO] Axiom selection finished. Selected 11 axioms (removed 0 axioms).
% 2.92/2.18 % [INFO] Problem is propositional (TPTP CNF).
% 2.92/2.19 % [INFO] Type checking passed.
% 2.92/2.19 % [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 ...
% 255.29/70.82 % External prover 'e' found a proof!
% 255.29/70.82 % [INFO] Killing All external provers ...
% 255.29/70.82 % Time passed: 70217ms (effective reasoning time: 69305ms)
% 255.29/70.82 % Axioms used in derivation (11): c05, c11, c08, c01, c03, c06, c02, c07, c10, c09, c04
% 255.29/70.82 % No. of inferences in proof: 1169
% 255.29/70.82 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p : 70217 ms resp. 69305 ms w/o parsing
% 253.39/71.01 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 253.39/71.02 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------